1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Fri Nov 29 17:43:34 2019 +0100
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Sat Nov 30 15:43:14 2019 +0100
     1.3 @@ -16,9 +16,6 @@
     1.4  (*declare [[ML_print_depth = 999]]*)
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
     1.8 -( *------------------------------------ rm libisabelle -----------------------------------------*)
     1.9 -(*\\---------------------------------- rm libisabelle ---------------------------------------//*)
    1.10  \<close> ML \<open>
    1.11  \<close> ML \<open>
    1.12  \<close>

     2.1 --- a/src/Tools/isac/CalcElements/calcelems.sml	Fri Nov 29 17:43:34 2019 +0100
     2.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml	Sat Nov 30 15:43:14 2019 +0100
     2.3 @@ -118,9 +118,10 @@
     2.4  val overwritelthy: theory -> (Rule.rls' * (string * Rule.rls)) list * (Rule.rls' * Rule.rls) list ->
     2.5    (Rule.rls' * (string * Rule.rls)) list  end
     2.6  
     2.7 -               
     2.8 +(**)
     2.9  structure Celem(**): CALC_ELEMENT(**) =
    2.10  struct
    2.11 +(**)
    2.12  
    2.13  val linefeed = (curry op^) "\n"; (* ?\<longrightarrow> libraryC ?*)
    2.14  type authors = string list;

     3.1 --- a/src/Tools/isac/Interpret/Interpret.thy	Fri Nov 29 17:43:34 2019 +0100
     3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy	Sat Nov 30 15:43:14 2019 +0100
     3.3 @@ -7,7 +7,6 @@
     3.4  imports "~~/src/Tools/isac/Specify/Specify"
     3.5  begin
     3.6  (* removed all warnings here, only "handle _" remains *)
     3.7 -  ML_file execute.sml
     3.8    ML_file rewtools.sml
     3.9    ML_file script.sml
    3.10    ML_file inform.sml

     4.1 --- a/src/Tools/isac/Interpret/execute.sml	Fri Nov 29 17:43:34 2019 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,16 +0,0 @@
     4.4 -(* Title:  interpreter-state for Lucas-Interpretation
     4.5 -   Author: Walther Neuper 190724
     4.6 -   (c) due to copyright terms
     4.7 -*)
     4.8 -signature EXECUTE =
     4.9 -sig
    4.10 -
    4.11 -end
    4.12 -
    4.13 -(**)
    4.14 -structure Exec(**): EXECUTE(**) =
    4.15 -struct
    4.16 -(**)
    4.17 -
    4.18 -end
    4.19 -

     5.1 --- a/src/Tools/isac/Interpret/inform.sml	Fri Nov 29 17:43:34 2019 +0100
     5.2 +++ b/src/Tools/isac/Interpret/inform.sml	Sat Nov 30 15:43:14 2019 +0100
     5.3 @@ -461,7 +461,7 @@
     5.4                val res = case rew of
     5.5                 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
     5.6                |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
     5.7 -              | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.tac_2str t)
     5.8 +              | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
     5.9              in 
    5.10                if not (ifo = res)
    5.11                then ("input does not exactly fill the gaps", Tactic.Tac "")

     6.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Fri Nov 29 17:43:34 2019 +0100
     6.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Nov 30 15:43:14 2019 +0100
     6.3 @@ -51,7 +51,8 @@
     6.4    val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
     6.5    val interpret_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
     6.6  
     6.7 -  datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term
     6.8 +  datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate * Proof.context
     6.9 +    | Reject_Tac2 | Term_Val2 of term
    6.10    val scan_dn2: Ctree.state * Proof.context -> Istate.pstate -> term -> expr_val2
    6.11    val scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> term -> expr_val2
    6.12    val go_scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> expr_val2
    6.13 @@ -123,7 +124,7 @@
    6.14           AssOnly => Term_Val1 act_arg
    6.15         | _(*ORundef*) =>
    6.16            case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
    6.17 -             Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Lucin.tac_2res m'), ctxt, tac)
    6.18 +             Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
    6.19             | Chead.Notappl _ => Term_Val1 act_arg)
    6.20  
    6.21  (** scan to a Prog_Tac **)
    6.22 @@ -288,7 +289,7 @@
    6.23            if assoc
    6.24            then Safe_Step (Istate.Pstate ist, ctxt, tac')
    6.25   	        else Unsafe_Step (Istate.Pstate ist, ctxt, tac')
    6.26 -      | Reject_Tac1 _ => Not_Locatable (Tactic.tac_2str tac ^ " not locatable")
    6.27 +      | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
    6.28        | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
    6.29    | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
    6.30  
    6.31 @@ -300,13 +301,14 @@
    6.32  
    6.33  (** scan to a Prog_Tac **)
    6.34  
    6.35 -datatype expr_val2 = (* "ExprVal" in the sense of denotational semantics        *)
    6.36 -  Reject_Tac2        (* tactic is found but NOT acknowledged, scan is continued *)
    6.37 -| Accept_Tac2 of       (* tactic is found and acknowledged, scan is stalled       *)
    6.38 -    Tactic.T *       (* Prog_Tac is applicable_in cstate                        *)
    6.39 -    Istate.pstate    (* the current state, returned for resuming execution      *)
    6.40 -| Term_Val2 of       (* Prog_Expr is found and evaluated, scan is continued     *)
    6.41 -    term;            (* value of Prog_Expr, for updating environment            *)
    6.42 +datatype expr_val2 = (* "ExprVal" in the sense of denotational semantics           *)
    6.43 +  Reject_Tac2        (* tactic is found but NOT acknowledged, scan is continued    *)
    6.44 +| Accept_Tac2 of     (* tactic is found and acknowledged, scan is stalled          *)
    6.45 +    Tactic.T *       (* Prog_Tac is applicable_in cstate                           *)
    6.46 +    Istate.pstate *  (* created by application of Tactic.T, for resuming execution *)
    6.47 +    Proof.context    (* created by application of Tactic.T                         *)
    6.48 +| Term_Val2 of       (* Prog_Expr is found and evaluated, scan is continued        *)
    6.49 +    term;            (* value of Prog_Expr, for updating environment               *)
    6.50  
    6.51  (*
    6.52    scan_dn2, go_scan_up2, scan_up2 scan for determine_next_tactic.
    6.53 @@ -376,10 +378,12 @@
    6.54    	      val (m, m') = Lucin.stac2tac_ pt (Proof_Context.theory_of ctxt) stac
    6.55          in
    6.56            case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
    6.57 -    	      Tactic.Subproblem _ => Accept_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
    6.58 +    	      Tactic.Subproblem _ =>
    6.59 +    	        Accept_Tac2 (m', ist |> set_subst_reset (a', Tactic.result m'), ctxt)
    6.60      	    | _ =>
    6.61              (case Applicable.applicable_in p pt m of
    6.62 -    		      Chead.Appl m' => Accept_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
    6.63 +    		      Chead.Appl m' => Accept_Tac2 (m',
    6.64 +    		        ist |> set_subst_reset (a', Tactic.result m'), Tactic.insert_assumptions m' ctxt)
    6.65      		    | _ => Reject_Tac2)
    6.66    	    end
    6.67  
    6.68 @@ -487,8 +491,8 @@
    6.69            (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe)))
    6.70      | Reject_Tac2 =>
    6.71          (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
    6.72 -    | Accept_Tac2 (m', (ist as {act_arg, ...})) =>
    6.73 -        (m', (Pstate ist, ctxt), (act_arg, Telem.Safe)))                  (* found next tac *)
    6.74 +    | Accept_Tac2 (m', (ist as {act_arg, ...}), ctxt) =>
    6.75 +        (m', (Pstate ist, Tactic.insert_assumptions m' ctxt), (act_arg, Telem.Safe)))                  (* found next tac *)
    6.76    | determine_next_tactic _ _  is _ =
    6.77      error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
    6.78  

     7.1 --- a/src/Tools/isac/Interpret/script.sml	Fri Nov 29 17:43:34 2019 +0100
     7.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat Nov 30 15:43:14 2019 +0100
     7.3 @@ -28,7 +28,6 @@
     7.4    val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tactic.input list
     7.5  (*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
     7.6    val stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
     7.7 -  val tac_2res : Tactic.T -> term
     7.8    val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
     7.9    val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
    7.10    val interpret_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
    7.11 @@ -377,56 +376,10 @@
    7.12    | associate _ _ (m, _) = 
    7.13      (if (!trace_script) 
    7.14       then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
    7.15 -		   ^ "@@@ tac_ = " ^ Tactic.tac_2str m)
    7.16 +		   ^ "@@@ tac_ = " ^ Tactic.string_of m)
    7.17       else ();
    7.18      NotAss);
    7.19  
    7.20 -fun make_rule thy t =
    7.21 -  let val ct = Thm.global_cterm_of thy (HOLogic.Trueprop $ t)
    7.22 -  in Rule.Thm (Rule.term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
    7.23 -
    7.24 -fun rep_tac_ (Tactic.Rewrite_Inst' (thy', _, _, _, subs, (thmID, _), f, (f', _))) = 
    7.25 -    let
    7.26 -      val subs' = Selem.subst_to_subst' subs;
    7.27 -      val sT' = type_of subs';
    7.28 -      val fT = type_of f;
    7.29 -      val lhs = Const ("Prog_Tac.Rewrite'_Inst", [sT', HOLogic.stringT, fT] ---> fT) 
    7.30 -        $ subs' $ HOLogic.mk_string thmID $ f;
    7.31 -    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
    7.32 -  | rep_tac_ (Tactic.Rewrite' (thy', _, _, _, (thmID, _), f, (f', _)))=
    7.33 -    let 
    7.34 -      val fT = type_of f;
    7.35 -      val lhs = Const ("Prog_Tac.Rewrite", [HOLogic.stringT, fT] ---> fT)
    7.36 -        $ HOLogic.mk_string thmID $ f;
    7.37 -    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
    7.38 -  | rep_tac_ (Tactic.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
    7.39 -    let
    7.40 -      val subs' = Selem.subst_to_subst' subs;
    7.41 -      val sT' = type_of subs';
    7.42 -      val fT = type_of f;
    7.43 -      val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, fT] ---> fT) 
    7.44 -        $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ f;
    7.45 -    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
    7.46 -  | rep_tac_ (Tactic.Rewrite_Set' (thy', _, rls, f, (f', _))) =
    7.47 -    let 
    7.48 -      val fT = type_of f;
    7.49 -      val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT) 
    7.50 -        $ HOLogic.mk_string (Rule.id_rls rls) $ f;
    7.51 -    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
    7.52 -  | rep_tac_ (Tactic.Calculate' (thy', op_, f, (f', _)))=
    7.53 -    let
    7.54 -      val fT = type_of f;
    7.55 -      val lhs = Const ("Prog_Tac.Calculate",[HOLogic.stringT,fT] ---> fT) $ HOLogic.mk_string op_ $ f
    7.56 -    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
    7.57 -  | rep_tac_ (Tactic.Check_elementwise' (_, _, (t', _))) = (Rule.Erule, (Rule.e_term, t'))
    7.58 -  | rep_tac_ (Tactic.Subproblem' (_, _, _, _, _, t')) = (Rule.Erule, (Rule.e_term, t'))
    7.59 -  | rep_tac_ (Tactic.Take' t') = (Rule.Erule, (Rule.e_term, t'))
    7.60 -  | rep_tac_ (Tactic.Substitute' (_, _, _, t, t')) = (Rule.Erule, (t, t'))
    7.61 -  | rep_tac_ (Tactic.Or_to_List' (t, t')) = (Rule.Erule, (t, t'))
    7.62 -  | rep_tac_ m = error ("rep_tac_: not impl.for " ^ Tactic.tac_2str m)
    7.63 -
    7.64 -fun tac_2res m = (snd o snd o rep_tac_) m;
    7.65 -
    7.66  (* create the initial interpreter state
    7.67    from the items of the guard and the formal arguments of the partial_function.
    7.68  Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
    7.69 @@ -679,6 +632,5 @@
    7.70            | _ => error "")
    7.71            (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
    7.72        in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;
    7.73 -(**)
    7.74 -end
    7.75 -(**)
    7.76 +
    7.77 +(**)end(**)

     8.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Fri Nov 29 17:43:34 2019 +0100
     8.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Sat Nov 30 15:43:14 2019 +0100
     8.3 @@ -179,7 +179,7 @@
     8.4    list;
     8.5  
     8.6  fun ets2s (l,(m,eno,env,iar,res,s)) = 
     8.7 -  "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.tac_2str m ^
     8.8 +  "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.string_of m ^
     8.9    ",\n  ens= " ^ Env.subst2str eno ^
    8.10    ",\n  env= " ^ Env.subst2str env ^
    8.11    ",\n  iar= " ^ Rule.term2str iar ^

     9.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Nov 29 17:43:34 2019 +0100
     9.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Sat Nov 30 15:43:14 2019 +0100
     9.3 @@ -54,7 +54,7 @@
     9.4    | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
     9.5    | Tac_ of theory * string * string * string
     9.6    | Take' of term | Take_Inst' of term
     9.7 -  val tac_2str : T -> string
     9.8 +  val string_of : T -> string
     9.9  
    9.10    datatype input =
    9.11      Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
    9.12 @@ -103,14 +103,17 @@
    9.13    | Take of Rule.cterm' | Take_Inst of Rule.cterm'
    9.14    val tac2str : input -> string
    9.15  
    9.16 -  val eq_tac : input * input -> bool                                              (* for script.sml *)
    9.17 -  val is_empty_tac : input -> bool                                              (* also for tests *)
    9.18 -  val is_rewtac : input -> bool                                              (* for interface.sml *)
    9.19 -  val is_rewset : input -> bool                                             (* for mathengine.sml *)
    9.20 -  val rls_of : input -> Rule.rls'                                               (* for solve.sml *)
    9.21 +  val eq_tac : input * input -> bool
    9.22 +  val is_empty_tac : input -> bool
    9.23 +  val is_rewtac : input -> bool
    9.24 +  val is_rewset : input -> bool
    9.25 +  val rls_of : input -> Rule.rls'
    9.26    val tac2IDstr : input -> string
    9.27 -  val rule2tac : theory -> (term * term) list ->  Rule.rule -> input         (* for rewtools.sml *)
    9.28 +  val rule2tac : theory -> (term * term) list ->  Rule.rule -> input
    9.29    val input_from_T : T -> input
    9.30 +  val result : T -> term
    9.31 +  val creates_assms: T -> term list
    9.32 +  val insert_assumptions: T -> Proof.context -> Proof.context
    9.33  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    9.34    (* NONE *)
    9.35  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    9.36 @@ -121,8 +124,10 @@
    9.37    (* NONE *)
    9.38  end
    9.39  
    9.40 +(**)
    9.41  structure Tactic(**): TACTIC(**) =
    9.42  struct
    9.43 +(**)
    9.44  
    9.45  (* tactics for user at front-end.
    9.46     input propagates the construction of the calc-tree;
    9.47 @@ -395,7 +400,7 @@
    9.48    | Tac_ of theory * string * string * string
    9.49    | Take' of term | Take_Inst' of term
    9.50  
    9.51 -fun tac_2str ma = case ma of
    9.52 +fun string_of ma = case ma of
    9.53      Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
    9.54    | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
    9.55    | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
    9.56 @@ -444,7 +449,7 @@
    9.57  
    9.58    | Empty_Tac_ => "Empty_Tac_"
    9.59    | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
    9.60 -  | _  => "tac_2str not impl. for arg";
    9.61 +  | _  => "string_of not impl. for arg";
    9.62  
    9.63  fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
    9.64    | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
    9.65 @@ -478,6 +483,24 @@
    9.66    | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
    9.67    | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
    9.68    | input_from_T Empty_Tac_ = Empty_Tac
    9.69 -  | input_from_T m = error (": not impl. for "^(tac_2str m));
    9.70 +  | input_from_T m = error (": not impl. for "^(string_of m));
    9.71  
    9.72 -end
    9.73 +fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
    9.74 +  | res (Rewrite' (_, _, _, _, _, _, res)) = res
    9.75 +  | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
    9.76 +  | res (Rewrite_Set' (_, _, _, _, res)) = res
    9.77 +  | res (Calculate' (_, _, _, (t, _))) = (t, [])
    9.78 +  | res (Check_elementwise' (_, _, res)) = res
    9.79 +  | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
    9.80 +  | res (Take' t) = (t, [])
    9.81 +  | res (Substitute' (_, _, _, _, t)) = (t, [])
    9.82 +  | res (Or_to_List' (_,  t)) = (t, [])
    9.83 +  | res m = raise ERROR ("result: not impl.for " ^ string_of m)
    9.84 +
    9.85 +(*fun result m = (fst o res) m; TODO*)
    9.86 +fun result tac = (fst o res) tac;
    9.87 +fun creates_assms tac = (snd o res) tac;
    9.88 +
    9.89 +fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt
    9.90 +
    9.91 +(**)end(**)

    10.1 --- a/src/Tools/isac/Specify/calchead.sml	Fri Nov 29 17:43:34 2019 +0100
    10.2 +++ b/src/Tools/isac/Specify/calchead.sml	Sat Nov 30 15:43:14 2019 +0100
    10.3 @@ -926,7 +926,7 @@
    10.4  	          nxt, Telem.Safe, pt)
    10.5            end
    10.6        end
    10.7 -  | specify m' _ _ _ = error ("specify: not impl. for " ^ Tactic.tac_2str m')
    10.8 +  | specify m' _ _ _ = error ("specify: not impl. for " ^ Tactic.string_of m')
    10.9  
   10.10  (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
   10.11    -- for input from scratch*)
   10.12 @@ -1278,7 +1278,7 @@
   10.13         ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Tactic.Refine_Tacitly pblID) ptp)
   10.14       | _ => (snd3 o hd o fst3) (nxt_specif Tactic.Model_Problem ptp))
   10.15         (*all stored in tac_ itms^^^^^^^^^^*)
   10.16 -  | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ Tactic.tac_2str tac_)
   10.17 +  | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ Tactic.string_of tac_)
   10.18  
   10.19  (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
   10.20    + met from fmz; assumes pos on PblObj, meth = []                    *)

    11.1 --- a/src/Tools/isac/Specify/generate.sml	Fri Nov 29 17:43:34 2019 +0100
    11.2 +++ b/src/Tools/isac/Specify/generate.sml	Sat Nov 30 15:43:14 2019 +0100
    11.3 @@ -96,7 +96,7 @@
    11.4      (Istate.T * Proof.context)))  (* after applying tac_, for ctree generation *)
    11.5  val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate.e_istate, ContextC.e_ctxt))): taci
    11.6  fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
    11.7 -  "( " ^ Tactic.tac2str tac ^ ", " ^ Tactic.tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
    11.8 +  "( " ^ Tactic.tac2str tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
    11.9    Istate.istate2str istate ^ " ))"
   11.10  fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
   11.11  
   11.12 @@ -369,7 +369,7 @@
   11.13      in
   11.14        ((p, Pbl), c, FormKF f, pt)
   11.15      end
   11.16 -  | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ Tactic.tac_2str m')
   11.17 +  | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ Tactic.string_of m')
   11.18  
   11.19  fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
   11.20    let
   11.21 @@ -409,7 +409,7 @@
   11.22  
   11.23  fun res_from_taci (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
   11.24    | res_from_taci (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
   11.25 -  | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ Tactic.tac_2str tac_)
   11.26 +  | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ Tactic.string_of tac_)
   11.27  
   11.28  (* embed the tacis created by a '_deriv'ation; sys.form <> input.form
   11.29    tacis are in order, thus are reverted for generate *)

    12.1 --- a/test/Tools/isac/CalcElements/contextC.sml	Fri Nov 29 17:43:34 2019 +0100
    12.2 +++ b/test/Tools/isac/CalcElements/contextC.sml	Sat Nov 30 15:43:14 2019 +0100
    12.3 @@ -10,7 +10,7 @@
    12.4  "-----------------------------------------------------------------------------------------------";
    12.5  "----------- fun initialise --------------------------------------------------------------------";
    12.6  "----------- build fun initialise'--------------------------------------------------------------";
    12.7 -"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
    12.8 +"----------- fun get_assumptions, fun ContextC.insert_assumptions----------------------------------------";
    12.9  "----------- fun transfer_asms_from_to ---------------------------------------------------------";
   12.10  "----------- fun from_subpbl_to_caller ---------------------------------------------------------";
   12.11  "----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
   12.12 @@ -47,11 +47,11 @@
   12.13      val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct
   12.14      val _ = TermC.raise_type_conflicts ts;
   12.15  
   12.16 -"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
   12.17 -"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
   12.18 -"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
   12.19 -val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
   12.20 -val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
   12.21 +"----------- fun get_assumptions, fun ContextC.insert_assumptions----------------------------------------";
   12.22 +"----------- fun get_assumptions, fun ContextC.insert_assumptions----------------------------------------";
   12.23 +"----------- fun get_assumptions, fun ContextC.insert_assumptions----------------------------------------";
   12.24 +val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
   12.25 +val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
   12.26  val asms = get_assumptions ctxt;
   12.27  if asms = [@{term "x * v"}, @{term "2 * u"}]
   12.28  then () else error "mstools.sml insert_/get_assumptions changed 1.";
   12.29 @@ -60,9 +60,9 @@
   12.30  "----------- fun transfer_asms_from_to ---------------------------------------------------------";
   12.31  "----------- fun transfer_asms_from_to ---------------------------------------------------------";
   12.32  val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
   12.33 -val from_ctxt = insert_assumptions
   12.34 +val from_ctxt = ContextC.insert_assumptions
   12.35    [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
   12.36 -val to_ctxt = insert_assumptions
   12.37 +val to_ctxt = ContextC.insert_assumptions
   12.38    [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
   12.39  val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
   12.40  if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
   12.41 @@ -72,9 +72,9 @@
   12.42  "----------- fun from_subpbl_to_caller ---------------------------------------------------------";
   12.43  "----------- fun from_subpbl_to_caller ---------------------------------------------------------";
   12.44  val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
   12.45 -val sub_ctxt = insert_assumptions
   12.46 +val sub_ctxt = ContextC.insert_assumptions
   12.47    [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
   12.48 -val caller_ctxt = insert_assumptions
   12.49 +val caller_ctxt = ContextC.insert_assumptions
   12.50    [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
   12.51  val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]";
   12.52  val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt;

    13.1 --- a/test/Tools/isac/Interpret/execute.sml	Fri Nov 29 17:43:34 2019 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,15 +0,0 @@
    13.4 -(* Title:  "Interpret/execute.sml"
    13.5 -   Author: Walther Neuper
    13.6 -   (c) due to copyright terms
    13.7 -*)
    13.8 -
    13.9 -"-----------------------------------------------------------------------------------------------";
   13.10 -"table of contents -----------------------------------------------------------------------------";
   13.11 -"-----------------------------------------------------------------------------------------------";
   13.12 -"-----------------------------------------------------------------------------------------------";
   13.13 -"----------- fun xxx ---------------------------------------------------------------------------";
   13.14 -"----------- fun xxx ---------------------------------------------------------------------------";
   13.15 -"----------- fun xxx ---------------------------------------------------------------------------";
   13.16 -"-----------------------------------------------------------------------------------------------";
   13.17 -"-----------------------------------------------------------------------------------------------";
   13.18 -"-----------------------------------------------------------------------------------------------";

    14.1 --- a/test/Tools/isac/Interpret/script.sml	Fri Nov 29 17:43:34 2019 +0100
    14.2 +++ b/test/Tools/isac/Interpret/script.sml	Sat Nov 30 15:43:14 2019 +0100
    14.3 @@ -14,7 +14,6 @@
    14.4  "----------- fun formal_args -------------------------------------";
    14.5  "----------- fun dsc_valT ----------------------------------------";
    14.6  "----------- fun itms2args ---------------------------------------";
    14.7 -"----------- fun rep_tac_ ----------------------------------------";
    14.8  "----------- fun init_pstate -----------------------------------------------------------------";
    14.9  "-----------------------------------------------------------------";
   14.10  "-----------------------------------------------------------------";
   14.11 @@ -282,109 +281,6 @@
   14.12  > map (term_to_string''' thy) ts;
   14.13  ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
   14.14  *)
   14.15 -"----------- fun rep_tac_ ----------------------------------------";
   14.16 -"----------- fun rep_tac_ ----------------------------------------";
   14.17 -"----------- fun rep_tac_ ----------------------------------------";
   14.18 -(***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) = 
   14.19 -Fehlersuche 25.4.01
   14.20 -(a)----- als String zusammensetzen:
   14.21 -ML> term2str f; 
   14.22 -val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
   14.23 -ML> term2str f'; 
   14.24 -val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
   14.25 -ML> subs;
   14.26 -val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
   14.27 -> val tt = (Thm.term_of o the o (parse thy))
   14.28 -  "(Rewrite_Inst[(''bdv'',x)]diff_const (d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
   14.29 -> atomty tt;
   14.30 -ML> tracing (term2str tt); 
   14.31 -(Rewrite_Inst [(''bdv'',x)] diff_const  d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
   14.32 - #0 + d_d x (x ^^^ #2 + #3 * x)
   14.33 -
   14.34 -(b)----- laut rep_tac_:
   14.35 -> val ttt=HOLogic.mk_eq (lhs,f');
   14.36 -> atomty ttt;
   14.37 -
   14.38 -
   14.39 -(*Fehlersuche 1-2Monate vor 4.01:*)
   14.40 -> val tt = (Thm.term_of o the o (parse thy))
   14.41 -  "Rewrite_Inst[(''bdv'',x)]square_equation_left True(x=#1+#2)";
   14.42 -> atomty tt;
   14.43 -
   14.44 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
   14.45 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
   14.46 -> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
   14.47 -	       (Thm.term_of o the o (parse thy)) "x")];
   14.48 -> val sT = (type_of o fst o hd) subs;
   14.49 -> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
   14.50 -			      (map HOLogic.mk_prod subs);
   14.51 -> val sT' = type_of subs';
   14.52 -> val lhs = Const ("Prog_Tac.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT) 
   14.53 -  $ subs' $ Free (thmID,idT) $ @{term True} $ f;
   14.54 -> lhs = tt;
   14.55 -val it = true : bool
   14.56 -> rep_tac_ (Rewrite_Inst' 
   14.57 -	       ("Program","tless_true","eval_rls",false,subs,
   14.58 -		("square_equation_left",""),f,(f',[])));
   14.59 -*)
   14.60 -(****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
   14.61 -> val tt = (Thm.term_of o the o (parse thy)) (*____   ____..test*)
   14.62 -  "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
   14.63 -
   14.64 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
   14.65 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
   14.66 -> val Thm (id,thm) = 
   14.67 -  rep_tac_ (Rewrite' 
   14.68 -   ("Program","tless_true","eval_rls",false,
   14.69 -    ("square_equation_left",""),f,(f',[])));
   14.70 -> val SOME ct = parse thy   
   14.71 -  "Rewrite square_equation_left True (x=#1+#2)"; 
   14.72 -> rewrite_ Program.thy tless_true eval_rls true thm ct;
   14.73 -val it = SOME ("x = #3",[]) : (cterm * cterm list) option
   14.74 -*)
   14.75 -(****************************************  | rep_tac_ (Rewrite_Set_Inst' 
   14.76 -WN050824: type error ...
   14.77 -  let val fT = type_of f;
   14.78 -    val sT = (type_of o fst o hd) subs;
   14.79 -    val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
   14.80 -      (map HOLogic.mk_prod subs);
   14.81 -    val sT' = type_of subs';
   14.82 -    val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst",
   14.83 -		     [sT',idT,fT,fT] ---> fT) 
   14.84 -      $ subs' $ Free (id_rls rls,idT) $ b $ f;
   14.85 -  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
   14.86 -(* ... vals from Rewrite_Inst' ...
   14.87 -> rep_tac_ (Rewrite_Set_Inst' 
   14.88 -	       ("Program",false,subs,
   14.89 -		"isolate_bdv",f,(f',[])));
   14.90 -*)
   14.91 -(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
   14.92 -*)
   14.93 -(**************************************   | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
   14.94 -13.3.01:
   14.95 -val thy = assoc_thy thy';
   14.96 -val t = HOLogic.mk_eq (lhs,f');
   14.97 -make_rule thy t;
   14.98 ---------------------------------------------------
   14.99 -val lll = (Thm.term_of o the o (parse thy)) 
  14.100 -  "Rewrite_Set SqRoot_simplify (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
  14.101 -
  14.102 ---------------------------------------------------
  14.103 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
  14.104 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
  14.105 -> val Thm (id,thm) = 
  14.106 -  rep_tac_ (Rewrite_Set' 
  14.107 -   ("Program",false,"SqRoot_simplify",f,(f',[])));
  14.108 -val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
  14.109 -val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
  14.110 -*)
  14.111 -(*****************************************   | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
  14.112 -> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
  14.113 -  ... test-root-equ.sml: calculate ...
  14.114 -> val Appl m'=applicable_in p pt (Calculate "PLUS");
  14.115 -> val (lhs,_)=tac_2etac m';
  14.116 -> lhs'=lhs;
  14.117 -val it = true : bool*)
  14.118  
  14.119  "----------- fun init_pstate -----------------------------------------------------------------";
  14.120  "----------- fun init_pstate -----------------------------------------------------------------";

    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Sat Nov 30 15:43:14 2019 +0100
    15.3 @@ -0,0 +1,25 @@
    15.4 +(* Title:  "MathEngBasic/tactic.sml"
    15.5 +   Author: Walther Neuper
    15.6 +   (c) due to copyright terms
    15.7 +*)
    15.8 +
    15.9 +"-----------------------------------------------------------------------------------------------";
   15.10 +"table of contents -----------------------------------------------------------------------------";
   15.11 +"-----------------------------------------------------------------------------------------------";
   15.12 +"-----------------------------------------------------------------------------------------------";
   15.13 +"----------- fun result, fun creates_assms ---------------------------------------------------";
   15.14 +"-----------------------------------------------------------------------------------------------";
   15.15 +"-----------------------------------------------------------------------------------------------";
   15.16 +"-----------------------------------------------------------------------------------------------";
   15.17 +
   15.18 +"----------- fun result, fun creates_assms ---------------------------------------------------";
   15.19 +"----------- fun result, fun creates_assms ---------------------------------------------------";
   15.20 +"----------- fun result, fun creates_assms ---------------------------------------------------";
   15.21 +val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
   15.22 +val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
   15.23 +;
   15.24 +Rewrite': theory' * rew_ord' * rls * bool * thm'' * term * result -> T;
   15.25 +val tac = Rewrite' ("Diff", "dummy_ord", e_rls, true, thm'', f, res)
   15.26 +;
   15.27 +if (Tactic.result tac |> term2str) = "a / b" then () else error "creates_assms CHANGED";
   15.28 +if (Tactic.creates_assms tac |> terms2str) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";

    16.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Nov 29 17:43:34 2019 +0100
    16.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Sat Nov 30 15:43:14 2019 +0100
    16.3 @@ -334,7 +334,8 @@
    16.4  val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
    16.5  if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
    16.6  else error "autoCalculate..CompleteCalc: final result";
    16.7 -if terms2strs (get_assumptions_ pt p) = ["matches (?a = ?b) (-1 + x = 0)", "x = 1", "precond_rootmet x"]
    16.8 +if eq_set op = (terms2strs (get_assumptions_ pt p),
    16.9 +  ["precond_rootmet 1", "matches (?a = ?b) (-1 + x = 0)", "x = 1", "precond_rootmet x"])
   16.10  (* assumptions are handled by Proof.context now:
   16.11    ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*) 
   16.12     "x = 1",                          (*result of subpbl and rootpbl*)
   16.13 @@ -515,12 +516,12 @@
   16.14                                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
   16.15  "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))), 
   16.16    (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac_Knowledge"), tac_, is, pos, pt);
   16.17 -        val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
   16.18 +        val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
   16.19            (Rewrite thm') (f',asm) Complete;
   16.20  (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
   16.21                                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
   16.22  "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = 
   16.23 -  (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
   16.24 +  (pt, p, (is, ContextC.insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
   16.25  existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
   16.26  apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
   16.27  apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;

    17.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Fri Nov 29 17:43:34 2019 +0100
    17.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Sat Nov 30 15:43:14 2019 +0100
    17.3 @@ -57,7 +57,7 @@
    17.4  val thy = assoc_thy thy';
    17.5  val {srls, pre, prls, ...} = get_met mI;
    17.6  val pres = check_preconds thy prls pre meth |> map snd;
    17.7 -val ctxt = ctxt |> insert_assumptions pres;
    17.8 +val ctxt = ctxt |> ContextC.insert_assumptions pres;
    17.9  val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI;
   17.10  "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI)
   17.11      val actuals = itms2args thy metID itms
   17.12 @@ -157,7 +157,7 @@
   17.13  (*+*)| _ => error "stac2tac_ changed"
   17.14  "~~~~~ continue last scan_dn2";
   17.15  val Chead.Appl m' = Applicable.applicable_in p pt m;
   17.16 -"~~~~~ fun tac_2res, args:"; val (m) = (m');
   17.17 +"~~~~~ fun result, args:"; val (m) = (m');
   17.18  "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
   17.19        val fT = type_of f;
   17.20        val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT) 

    18.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Fri Nov 29 17:43:34 2019 +0100
    18.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Sat Nov 30 15:43:14 2019 +0100
    18.3 @@ -108,13 +108,13 @@
    18.4  "~~~~~ fun determine_next_tactic , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
    18.5    = (sc, (pt, pos), ist, ctxt);
    18.6  
    18.7 -val Accept_Tac2 (Rewrite_Set' _, _) = (*case*)
    18.8 +val Accept_Tac2 (Rewrite_Set' _, _, _) = (*case*)
    18.9             scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
   18.10  "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
   18.11    = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
   18.12    (*if*) 0 = length path (*else*);
   18.13  
   18.14 -val Accept_Tac2 (Rewrite_Set' _, _) =
   18.15 +val Accept_Tac2 (Rewrite_Set' _, _, _) =
   18.16             go_scan_up2 (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);
   18.17  "~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...})) =
   18.18    ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));
   18.19 @@ -162,7 +162,7 @@
   18.20  "~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
   18.21    = (sc, (pt, pos), ist, ctxt);
   18.22  
   18.23 -val Accept_Tac2 (_, _) = (*case*)
   18.24 +val Accept_Tac2 (_, _, _) = (*case*)
   18.25             scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
   18.26  "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
   18.27    = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
   18.28 @@ -210,7 +210,7 @@
   18.29  "~~~~~ fun scan_dn2 , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b))))
   18.30    = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
   18.31  
   18.32 -  val Accept_Tac2 (Subproblem' _, _) = (*case*)
   18.33 +  val Accept_Tac2 (Subproblem' _, _, _) = (*case*)
   18.34             scan_dn2 xxx (ist |> path_down [L, R]) e (*of*);
   18.35      (*========== a leaf has been found ==========*)   
   18.36  "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t)

    19.1 --- a/test/Tools/isac/Specify/appl.sml	Fri Nov 29 17:43:34 2019 +0100
    19.2 +++ b/test/Tools/isac/Specify/appl.sml	Sat Nov 30 15:43:14 2019 +0100
    19.3 @@ -40,7 +40,7 @@
    19.4  if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then ()
    19.5  else error "appl.sml Apply_Method diff.behav.";
    19.6  
    19.7 -val ctxt = assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres;
    19.8 +val ctxt = assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres;
    19.9  (*TODO.WN110416 read pres from ctxt and check*)
   19.10  
   19.11  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    20.1 --- a/test/Tools/isac/Specify/generate.sml	Fri Nov 29 17:43:34 2019 +0100
    20.2 +++ b/test/Tools/isac/Specify/generate.sml	Sat Nov 30 15:43:14 2019 +0100
    20.3 @@ -57,9 +57,9 @@
    20.4  
    20.5      val (pt,c) = 
    20.6        case subs_opt of
    20.7 -        NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
    20.8 +        NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
    20.9            (Rewrite thm') (f', []) Inconsistent
   20.10 -      | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
   20.11 +      | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
   20.12            (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
   20.13      val pt = update_branch pt p' TransitiveB;
   20.14  

    21.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Nov 29 17:43:34 2019 +0100
    21.2 +++ b/test/Tools/isac/Test_Isac.thy	Sat Nov 30 15:43:14 2019 +0100
    21.3 @@ -104,7 +104,6 @@
    21.4    open Math_Engine;            CalcTreeTEST;
    21.5    open Lucin;                  itms2args;
    21.6    open Env;
    21.7 -  open Exec;
    21.8    open LucinNEW;               scan_dn2;
    21.9    open Istate;
   21.10    open Inform;                 cas_input;
   21.11 @@ -215,7 +214,6 @@
   21.12    ML_file "Specify/calchead.sml"
   21.13    ML_file "Specify/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"   *)
   21.14  
   21.15 -  ML_file "Interpret/execute.sml"
   21.16    ML_file "Interpret/rewtools.sml"
   21.17    ML_file "Interpret/script.sml"
   21.18    ML_file "Interpret/inform.sml"

    22.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Nov 29 17:43:34 2019 +0100
    22.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sat Nov 30 15:43:14 2019 +0100
    22.3 @@ -100,7 +100,6 @@
    22.4    open Math_Engine;            CalcTreeTEST;
    22.5    open Lucin;                  itms2args;
    22.6    open Env;
    22.7 -  open Exec;
    22.8    open LucinNEW;               scan_dn2;
    22.9    open Istate;
   22.10    open Inform;                 cas_input;
   22.11 @@ -121,7 +120,7 @@
   22.12    open Selem;                  e_fmz;
   22.13    open Stool;                  (* NONE *)
   22.14    open ContextC;               transfer_asms_from_to;
   22.15 -  open Tactic;                 (* NONE *)
   22.16 +  open Tactic;                 insert_assumptions;
   22.17    open Model;                  (* NONE *)
   22.18    open Rewrite;                mk_thm;
   22.19    open Calc;                   get_pair;
   22.20 @@ -207,6 +206,7 @@
   22.21    ML_file "MathEngBasic/model.sml"
   22.22    ML_file "MathEngBasic/mstools.sml"
   22.23    ML_file "MathEngBasic/specification-elems.sml"
   22.24 +  ML_file "MathEngBasic/tactic.sml"
   22.25    ML_file "MathEngBasic/ctree.sml"         (*!...!see(25)*)
   22.26    ML_file "Specify/ptyps.sml"         (* requires setup from ptyps.thy *)
   22.27    ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
   22.28 @@ -214,11 +214,11 @@
   22.29    ML_file "Specify/calchead.sml"
   22.30    ML_file "Specify/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"   *)
   22.31  
   22.32 -  ML_file "Interpret/execute.sml"
   22.33    ML_file "Interpret/rewtools.sml"
   22.34    ML_file "Interpret/script.sml"
   22.35    ML_file "Interpret/inform.sml"
   22.36    ML_file "Interpret/lucas-interpreter.sml"
   22.37 +
   22.38    ML_file "MathEngine/solve.sml"
   22.39    ML_file "MathEngine/mathengine-stateless.sml"    (*!part. WN130804: +check Interpret/me.sml*)
   22.40    ML_file "MathEngine/messages.sml"

    23.1 --- a/test/Tools/isac/Test_Some.thy	Fri Nov 29 17:43:34 2019 +0100
    23.2 +++ b/test/Tools/isac/Test_Some.thy	Sat Nov 30 15:43:14 2019 +0100
    23.3 @@ -10,7 +10,6 @@
    23.4    open Math_Engine;            CalcTreeTEST;
    23.5    open Lucin;                  itms2args;
    23.6    open Env;
    23.7 -  open Exec;
    23.8    open LucinNEW;               scan_dn2;
    23.9    open Istate;
   23.10    open Inform;                 cas_input;
   23.11 @@ -84,6 +83,15 @@
   23.12  "~~~~~ fun xxx , args:"; val () = ();
   23.13  \<close>
   23.14  
   23.15 +section \<open>===================================================================================\<close>
   23.16 +ML \<open>
   23.17 +"~~~~~ fun xxx , args:"; val () = ();
   23.18 +\<close> ML \<open>
   23.19 +\<close> ML \<open>
   23.20 +\<close> ML \<open>
   23.21 +"~~~~~ fun xxx , args:"; val () = ();
   23.22 +\<close>
   23.23 +
   23.24  section \<open>================ test/../lucas-interpreter.sml =====================\<close>
   23.25  ML \<open>
   23.26  "----------- re-build: fun determine_next_tactic -----------------------------------------------";
   23.27 @@ -129,7 +137,7 @@
   23.28  "~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, ptp as(pt, (p, _)), Istate.Pstate ist, ctxt)
   23.29    = (sc, (pt, pos), ist, ctxt);
   23.30  \<close> ML \<open>
   23.31 -(*OLD*)val Accept_Tac2 (m',        (ist as {act_arg, ...})) =
   23.32 +(*OLD*)val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =
   23.33  (*OLD*)  (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
   23.34  (*NEW*)
   23.35  (*NEW*)
   23.36 @@ -148,7 +156,7 @@
   23.37  (*OLD*)  val _ = (*case*) tac_'''''_' (*of*);
   23.38  (*OLD*)begin_end_prog tac_'''''_' is'''''_' ptp'''''_'  (*return value*);
   23.39  (*NEW*)
   23.40 -(*NEW*)
   23.41 +(*NEW*)                                                                                                                                
   23.42  \<close> ML \<open>
   23.43  "~~~~~ from and do_solve_step\<longrightarrow>fun step , return:"; val (tac_'''''_')
   23.44    = (begin_end_prog tac_'''''_' is ptp);