equal
deleted
inserted
replaced
41 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list |
41 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list |
42 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
42 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
43 |
43 |
44 end |
44 end |
45 |
45 |
46 (* traces the leaves (ie. non-tactical nodes) of Prog found by determine_next_tactic, see "and scr" *) |
46 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_tactic, see "and scr" *) |
47 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *) |
47 val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *) |
48 |
48 |
49 (**) |
49 (**) |
50 structure Lucin(**): LUCAS_INTERPRETER_DEL(**) = |
50 structure Lucin(**): LUCAS_INTERPRETER_DEL(**) = |
51 struct |
51 struct |