Ticket #452 (new bug)

Opened 2 years ago

Last modified 16 months ago

CoCasl - Isabelle tactics

Reported by: luecke Owned by: hausmann
Priority: critical Milestone: 0.95
Component: hets Version: 0.75
Keywords: Cc: lschrode

Description

Hets-lib/CoCASL/Proof-Support-Examples/tactics.ML does not work with Isabelle2007, because of changes in the ML-Interface.

E.g. a new version of build_tactic looks like this: 

 fun build_tactic tac = 
    Method.ctxt_args (fn ctxt => ((ML_Context.set_context (SOME
 (Context.Theory (ProofContext.theory_of ctxt))); Method.METHOD (fn facts
 => tac))))

Change History

Changed 16 months ago by luecke

  • cc lschrode added
  • priority changed from major to critical
  • milestone changed from 0.9 to 0.95
Note: See TracTickets for help on using tickets.