1.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Mon Apr 06 11:44:36 2020 +0200
     1.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml	Wed Apr 08 12:32:51 2020 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4   val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
     1.5  (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
     1.6  andalso Istate.string_of (get_istate_LI pt p)
     1.7 -  = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"
     1.8 +  = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
     1.9  then () else error "refFormula =   1 + -1 * 2 + x = 0   changed";
    1.10  (*-------------------------------------------------------------------------*)
    1.11  
    1.12 @@ -181,11 +181,11 @@
    1.13  (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
    1.14  Step.by_tactic : Tactic.input -> state -> string * (taci list * pos' list * state);
    1.15  if Istate.string_of istate
    1.16 - = "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)"
    1.17 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
    1.18  then () else error "from Step.by_tactic return --- changed 1";
    1.19  
    1.20  if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
    1.21 - = "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)"
    1.22 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
    1.23  then () else error "from Step.by_tactic return --- changed 2";
    1.24  (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
    1.25  
    1.26 @@ -204,7 +204,7 @@
    1.27  (*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
    1.28  (********************* locate_input_tactic returns cstate * istate * Proof.context  *************)
    1.29  (*+*)if Istate.string_of istate
    1.30 -(*+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)"
    1.31 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
    1.32  then case m of Rewrite_Set_Inst' _ => ()
    1.33  else error "from locate_input_tactic return --- changed";
    1.34  
    1.35 @@ -230,7 +230,7 @@
    1.36  (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
    1.37       Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
    1.38  (*+*)if pos' = ([1], Res) andalso Istate.string_of istate
    1.39 - = "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)"
    1.40 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
    1.41  then () else error "init. step 1 + -1 * 2 + x = 0 changed";
    1.42  
    1.43         val pIopt = get_pblID (pt,ip);
    1.44 @@ -242,7 +242,7 @@
    1.45  val ("ok", [], ptp as (pt, p)) = xxxx;
    1.46                                           
    1.47  if Istate.string_of (get_istate_LI pt p) (*                <>                 <>                 <>                 <>                     ^^^^^^^^^^^^^*)
    1.48 -(*REP*) = "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)"
    1.49 +(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
    1.50  then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
    1.51  
    1.52  "~~~~~ from TOPLEVEL to states return:";  upd_calc cI (ptp, []); upd_ipos cI 1 p;