test/Tools/isac/BridgeLibisabelle/use-cases.sml
changeset 59851 4dd533681fef
parent 59844 373d13915f8c
child 59852 ea7e6679080e
     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)"