1.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Apr 04 12:11:32 2020 +0200
1.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Apr 06 11:44:36 2020 +0200
1.3 @@ -201,7 +201,7 @@
1.4 val Safe_Step (istate, _, tac) =
1.5 (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
1.6
1.7 -(*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
1.8 +(*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
1.9 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
1.10 (*+*)if Istate.string_of istate
1.11 (*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"