1.1 --- a/src/Tools/isac/Interpret/inform.sml	Fri Jan 17 13:47:19 2020 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Fri Jan 17 14:10:10 2020 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4    type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec
     1.5    val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
     1.6    val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
     1.7 -  val find_fillpatterns : Ctree.state -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
     1.8 -  val is_exactly_equal : Ctree.state -> string -> string * Tactic.input
     1.9 +  val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
    1.10 +  val is_exactly_equal : Calc.T -> string -> string * Tactic.input
    1.11  (*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
    1.12    val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
    1.13      Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list

     2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Fri Jan 17 13:47:19 2020 +0100
     2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Fri Jan 17 14:10:10 2020 +0100
     2.3 @@ -9,29 +9,29 @@
     2.4        Safe_Step of Istate.T * Proof.context * Tactic.T
     2.5      | Unsafe_Step of Istate.T * Proof.context * Tactic.T
     2.6      | Not_Locatable of string
     2.7 -  val locate_input_tactic: Program.T -> Ctree.state -> Istate.T -> Proof.context -> Tactic.T
     2.8 +  val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context -> Tactic.T
     2.9      -> input_tactic_result
    2.10  
    2.11    datatype next_step_result =
    2.12        Next_Step of Istate.T * Proof.context * Tactic.T
    2.13      | Helpless | End_Program of Istate.T * Tactic.T
    2.14 -  val find_next_step: Program.T -> Ctree.state -> Istate.T -> Proof.context
    2.15 +  val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context
    2.16      -> next_step_result
    2.17  
    2.18 -(*TODO      input_term_result = Found_Step of  Ctree.state | Not_Derivable *)
    2.19 +(*TODO      input_term_result = Found_Step of  Calc.T | Not_Derivable *)
    2.20    datatype input_term_result =
    2.21 -    Found_Step of Ctree.state * Istate.T * Proof.context
    2.22 +    Found_Step of Calc.T * Istate.T * Proof.context
    2.23    | Not_Derivable of Chead.calcstate'
    2.24 -(*TODOlocate_input_formula: Ctree.state -> term -> input_term_result *)
    2.25 -  val locate_input_term: Program.T -> Ctree.state -> Istate.T -> Proof.context -> term
    2.26 +(*TODOlocate_input_formula: Calc.T -> term -> input_term_result *)
    2.27 +  val locate_input_term: Program.T -> Calc.T -> Istate.T -> Proof.context -> term
    2.28      -> input_term_result
    2.29                          
    2.30    (* must reside here:
    2.31       find_next_step calls do_next and is called by by_tactic;
    2.32       by_tactic and do_next are mutually recursive via by_tacti..Apply_Method'
    2.33     *)
    2.34 -  val by_tactic: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> string * Chead.calcstate'
    2.35 -  val do_next: Ctree.state -> string * Chead.calcstate'
    2.36 +  val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Chead.calcstate'
    2.37 +  val do_next: Calc.T -> string * Chead.calcstate'
    2.38  
    2.39  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    2.40    datatype expr_val1 =
    2.41 @@ -44,21 +44,21 @@
    2.42    datatype expr_val = Accept_Tac of Tactic.T * Istate.pstate * Proof.context
    2.43      | Reject_Tac | Term_Val of term
    2.44  
    2.45 -  val scan_dn: Ctree.state * Proof.context -> Istate.pstate -> term -> expr_val
    2.46 -  val scan_up: term * (Ctree.state * Proof.context) -> Istate.pstate -> term -> expr_val
    2.47 -  val go_scan_up: term * (Ctree.state * Proof.context) -> Istate.pstate -> expr_val
    2.48 -  val scan_to_tactic: term * (Ctree.state * Proof.context) -> Istate.T -> expr_val
    2.49 -  val check_tac: Ctree.state * Proof.context -> Istate.pstate -> term option * term -> expr_val;
    2.50 +  val scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val
    2.51 +  val scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val
    2.52 +  val go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val
    2.53 +  val scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val
    2.54 +  val check_tac: Calc.T * Proof.context -> Istate.pstate -> term option * term -> expr_val;
    2.55  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    2.56    val check_Let_up: Istate.pstate -> term -> term * term
    2.57 -  val compare_step: Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
    2.58 +  val compare_step: Generate.taci list * Ctree.pos' list * (Calc.T) -> term -> string * Chead.calcstate'
    2.59  
    2.60 -  val scan_dn1: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
    2.61 -  val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
    2.62 -  val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
    2.63 -  val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
    2.64 +  val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
    2.65 +  val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
    2.66 +  val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
    2.67 +  val scan_to_tactic1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.T -> expr_val1
    2.68  
    2.69 -  val check_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
    2.70 +  val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
    2.71  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.72  end
    2.73  
    2.74 @@ -500,7 +500,7 @@
    2.75  (*** locate an input formula in the program ***)
    2.76  
    2.77  datatype input_term_result =
    2.78 -    Found_Step of Ctree.state * Istate.T * Proof.context
    2.79 +    Found_Step of Calc.T * Istate.T * Proof.context
    2.80    | Not_Derivable of Chead.calcstate'
    2.81  
    2.82  fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
    2.83 @@ -648,7 +648,7 @@
    2.84     ALTERNATIVE: check_error_patterns _within_ compare_step: seems too expensive
    2.85  *)
    2.86  (*                       vvvv           vvvvvv vvvv    NEW args for compare_step *)
    2.87 -fun locate_input_term (Rule.Prog _)  ((pt, pos) : Ctree.state) (_ : Istate.T) (_ : Proof.context) tm =
    2.88 +fun locate_input_term (Rule.Prog _)  ((pt, pos) : Calc.T) (_ : Istate.T) (_ : Proof.context) tm =
    2.89       let                                                          
    2.90     		val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
    2.91     		val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)

     3.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Fri Jan 17 13:47:19 2020 +0100
     3.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Fri Jan 17 14:10:10 2020 +0100
     3.3 @@ -33,7 +33,7 @@
     3.4    val subs_from : Istate.T -> 'a -> Celem.guh -> Selem.subs
     3.5    val guh2rewtac : Celem.guh -> Selem.subs -> Tactic.input
     3.6    val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Tactic.input
     3.7 -  val context_thy : Ctree.state -> Tactic.input -> contthy
     3.8 +  val context_thy : Calc.T -> Tactic.input -> contthy
     3.9    val distinct_Thm : Rule.rule list -> Rule.rule list
    3.10    val eq_Thms : string list -> Rule.rule -> bool
    3.11    val make_deriv : theory -> Rule.rls -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->

     4.1 --- a/src/Tools/isac/Interpret/script.sml	Fri Jan 17 13:47:19 2020 +0100
     4.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri Jan 17 14:10:10 2020 +0100
     4.3 @@ -18,7 +18,7 @@
     4.4    val init_form : 'a -> Program.T -> (term * term) list -> term option
     4.5    val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T
     4.6  
     4.7 -  val get_simplifier : Ctree.state -> Rule.rls
     4.8 +  val get_simplifier : Calc.T -> Rule.rls
     4.9  (*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
    4.10      Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
    4.11  (*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> 

     5.1 --- a/src/Tools/isac/Interpret/step-solve.sml	Fri Jan 17 13:47:19 2020 +0100
     5.2 +++ b/src/Tools/isac/Interpret/step-solve.sml	Fri Jan 17 14:10:10 2020 +0100
     5.3 @@ -5,8 +5,8 @@
     5.4  
     5.5  signature STEP_SOLVE =
     5.6  sig
     5.7 -  val by_tactic : Tactic.T -> Ctree.state -> string * Chead.calcstate'
     5.8 -  val do_next: Ctree.state -> string * Chead.calcstate'
     5.9 +  val by_tactic : Tactic.T -> Calc.T -> string * Chead.calcstate'
    5.10 +  val do_next: Calc.T -> string * Chead.calcstate'
    5.11  
    5.12  end
    5.13  

     6.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Jan 17 13:47:19 2020 +0100
     6.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Jan 17 14:10:10 2020 +0100
     6.3 @@ -9,19 +9,19 @@
     6.4    type NEW (* TODO: refactor "fun me" with calcstate and remove *)
     6.5    val me : Tactic.input -> Ctree.pos' -> NEW -> Ctree.ctree ->
     6.6      Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
     6.7 -  val autocalc : Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list ->
     6.8 -    Solve.auto -> string * Ctree.pos' list * (Ctree.state)
     6.9 +  val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list ->
    6.10 +    Solve.auto -> string * Ctree.pos' list * (Calc.T)
    6.11    val locatetac :
    6.12 -    Tactic.input -> Ctree.state -> string * (Generate.taci list * Ctree.pos' list * (Ctree.state))
    6.13 +    Tactic.input -> Calc.T -> string * (Generate.taci list * Ctree.pos' list * (Calc.T))
    6.14    val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
    6.15  
    6.16    val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
    6.17    val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
    6.18    val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list
    6.19    val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
    6.20 -  val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    6.21 -  val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    6.22 -  val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    6.23 +  val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    6.24 +  val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    6.25 +  val set_theory : Rule.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
    6.26    val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
    6.27  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    6.28    val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
    6.29 @@ -30,8 +30,8 @@
    6.30    type nxt_
    6.31    datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
    6.32    val loc_solve_ : Tactic.T -> Ctree.ctree *  Ctree.pos' -> lOc_
    6.33 -  val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
    6.34 -  val TESTg_form : Ctree.state -> Generate.mout
    6.35 +  val loc_specify_ : Tactic.T -> Calc.T -> lOc_
    6.36 +  val TESTg_form : Calc.T -> Generate.mout
    6.37  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.38  
    6.39  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

     7.1 --- a/src/Tools/isac/MathEngine/solve.sml	Fri Jan 17 13:47:19 2020 +0100
     7.2 +++ b/src/Tools/isac/MathEngine/solve.sml	Fri Jan 17 14:10:10 2020 +0100
     7.3 @@ -9,10 +9,10 @@
     7.4    | CompleteToSubpbl | Steps of int
     7.5    val autoord : auto -> int
     7.6  
     7.7 -  val all_solve : auto -> Ctree.pos' list -> Ctree.state ->
     7.8 +  val all_solve : auto -> Ctree.pos' list -> Calc.T ->
     7.9      string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))
    7.10    val complete_solve :
    7.11 -     auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state
    7.12 +     auto -> Ctree.pos' list -> Calc.T -> string * Ctree.pos' list * Calc.T
    7.13    val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
    7.14  
    7.15    val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'

     8.1 --- a/src/Tools/isac/MathEngine/step.sml	Fri Jan 17 13:47:19 2020 +0100
     8.2 +++ b/src/Tools/isac/MathEngine/step.sml	Fri Jan 17 14:10:10 2020 +0100
     8.3 @@ -13,7 +13,7 @@
     8.4   *)
     8.5  signature STEP =
     8.6  sig
     8.7 -  val specify_do_next: Ctree.state -> string * Chead.calcstate'
     8.8 +  val specify_do_next: Calc.T -> string * Chead.calcstate'
     8.9    val do_next : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
    8.10  
    8.11  end

     9.1 --- a/src/Tools/isac/Specify/calchead.sml	Fri Jan 17 13:47:19 2020 +0100
     9.2 +++ b/src/Tools/isac/Specify/calchead.sml	Fri Jan 17 14:10:10 2020 +0100
     9.3 @@ -74,23 +74,23 @@
     9.4    val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
     9.5      (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input
     9.6  
     9.7 -  val reset_calchead : Ctree.state -> Ctree.state
     9.8 -  val get_ocalhd : Ctree.state -> Ctree.ocalhd
     9.9 +  val reset_calchead : Calc.T -> Calc.T
    9.10 +  val get_ocalhd : Calc.T -> Ctree.ocalhd
    9.11    val ocalhd_complete : Model.itm list -> (bool * term) list -> Rule.domID * Celem.pblID * Celem.metID -> bool
    9.12 -  val all_modspec : Ctree.state -> Ctree.state 
    9.13 +  val all_modspec : Calc.T -> Calc.T 
    9.14  
    9.15    val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem.pat list -> Model.itm list
    9.16    val insert_ppc' : Model.itm -> Model.itm list -> Model.itm list
    9.17  
    9.18 -  val complete_mod : Ctree.state -> Ctree.state
    9.19 -  val is_complete_mod : Ctree.state -> bool
    9.20 -  val complete_spec : Ctree.state -> Ctree.state
    9.21 -  val is_complete_spec : Ctree.state -> bool
    9.22 +  val complete_mod : Calc.T -> Calc.T
    9.23 +  val is_complete_mod : Calc.T -> bool
    9.24 +  val complete_spec : Calc.T -> Calc.T
    9.25 +  val is_complete_spec : Calc.T -> bool
    9.26    val some_spec : Celem.spec -> Celem.spec -> Celem.spec
    9.27    (* these could go to Ctree ..*)
    9.28    val show_pt : Ctree.ctree -> unit
    9.29    val show_pt_tac : Ctree.ctree -> unit
    9.30 -  val pt_extract : Ctree.state -> Ctree.ptform * Tactic.input option * term list 
    9.31 +  val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list 
    9.32    val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term * Tactic.input option) list
    9.33  
    9.34    val match_ags : theory -> Celem.pat list -> term list -> Model.ori list
    9.35 @@ -106,10 +106,10 @@
    9.36    val nxt_add: theory -> Model.ori list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
    9.37    val is_error: Model.itm_ -> bool
    9.38    val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * Model.itm list -> Model.itm list * Model.itm list
    9.39 -  val nxt_specif_additem: string -> Rule.cterm' -> Ctree.state -> calcstate'
    9.40 +  val nxt_specif_additem: string -> Rule.cterm' -> Calc.T -> calcstate'
    9.41    val vals_of_oris : Model.ori list -> term list
    9.42  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    9.43 -  val e_calcstate : Ctree.state * Generate.taci list
    9.44 +  val e_calcstate : Calc.T * Generate.taci list
    9.45    val e_calcstate' : calcstate'
    9.46  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    9.47    val posterms2str : (pos' * term * 'a) list -> string
    9.48 @@ -137,7 +137,7 @@
    9.49    val chktyps : theory -> term list * term list -> term list (* only in old tests*)
    9.50    val chk_vars : term Model.ppc -> string * term list
    9.51    val unbound_ppc : term Model.ppc -> term list
    9.52 -  val is_complete_modspec : Ctree.state -> bool
    9.53 +  val is_complete_modspec : Calc.T -> bool
    9.54    val get_formress : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
    9.55      (string * Ctree.pos' * term) list
    9.56    val get_forms : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->

    10.1 --- a/src/Tools/isac/Specify/generate.sml	Fri Jan 17 13:47:19 2020 +0100
    10.2 +++ b/src/Tools/isac/Specify/generate.sml	Fri Jan 17 14:10:10 2020 +0100
    10.3 @@ -21,13 +21,13 @@
    10.4    val init_istate : Tactic.input -> term -> Istate_Def.T
    10.5    val init_pbl : (string * (term * 'a)) list -> Model.itm list
    10.6    val init_pbl' : (string * (term * term)) list -> Model.itm list
    10.7 -  val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)
    10.8 +  val embed_deriv : taci list -> Calc.T -> Ctree.pos' list * (Calc.T) (* for inform.sml *)
    10.9    val generate_hard : (* for solve.sml *)
   10.10      theory -> Tactic.T -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
   10.11    val generate : (Tactic.input * Tactic.T * (Ctree.pos' * (Istate_Def.T * Proof.context))) list ->
   10.12      Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
   10.13    val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Istate_Def.T * Proof.context ->
   10.14 -    Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
   10.15 +    Ctree.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
   10.16  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   10.17    val tacis2str : taci list -> string
   10.18    val mout2str : mout -> string

    11.1 --- a/src/Tools/isac/Specify/specify.sml	Fri Jan 17 13:47:19 2020 +0100
    11.2 +++ b/src/Tools/isac/Specify/specify.sml	Fri Jan 17 14:10:10 2020 +0100
    11.3 @@ -1,8 +1,8 @@
    11.4  signature SPECIFY_NEW =
    11.5  sig
    11.6 -  val find_next_step: Ctree.state -> string * (Pos.pos_ * Tactic.input)
    11.7 +  val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
    11.8    val nxt_specify_init_calc : Selem.fmz -> Chead.calcstate
    11.9 -  val nxt_model_pbl : Tactic.T -> Ctree.state -> Tactic.T
   11.10 +  val nxt_model_pbl : Tactic.T -> Calc.T -> Tactic.T
   11.11  
   11.12  end
   11.13  

    12.1 --- a/src/Tools/isac/Specify/step-specify.sml	Fri Jan 17 13:47:19 2020 +0100
    12.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Fri Jan 17 14:10:10 2020 +0100
    12.3 @@ -5,7 +5,7 @@
    12.4  
    12.5  signature STEP_SPECIFY =
    12.6  sig
    12.7 -  val by_tactic: Tactic.input -> Ctree.state -> Chead.calcstate'
    12.8 +  val by_tactic: Tactic.input -> Calc.T -> Chead.calcstate'
    12.9  (*val do_next: Step.specify_do_next requires LucinNEW.by_tactic, which is not yet known in Step_Specify*)
   12.10  
   12.11  end

    13.1 --- a/src/Tools/isac/TODO.thy	Fri Jan 17 13:47:19 2020 +0100
    13.2 +++ b/src/Tools/isac/TODO.thy	Fri Jan 17 14:10:10 2020 +0100
    13.3 @@ -74,14 +74,14 @@
    13.4          \begin{itemize}
    13.5          \item Step_Specify.check <-- Applicable.applicable_in
    13.6          \item Step_Specify.add   <-- Generate.generate1
    13.7 -        \item Step_Specify.by_formula: ?term?       -> Ctree.state -> ...stay as is
    13.8 +        \item Step_Specify.by_formula: ?term?       -> Calc.T -> ...stay as is
    13.9          \end{itemize}
   13.10        \item Step_Solve in Interpret/step-solve.sml
   13.11          \begin{itemize}
   13.12          \item Step_Solve.check   <-- Applicable.applicable_in
   13.13            inserts all data into Tactic.T available -- not all are at time of call!
   13.14          \item Step_Solve.add     <-- Generate.generate1
   13.15 -        \item Step_Solve.by_formula  : term         -> Ctree.state -> ...stay as is
   13.16 +        \item Step_Solve.by_formula  : term         -> Calc.T -> ...stay as is
   13.17          \end{itemize}
   13.18        \item Step in MathEngine/step.sml
   13.19          \begin{itemize}
   13.20 @@ -312,7 +312,7 @@
   13.21  \<close>
   13.22  subsection \<open>solve, loc_solve_, by_tactic, do_next, ...\<close>
   13.23  text \<open>
   13.24 -  unify to calcstate, calcstate', ?Ctree.state?
   13.25 +  unify to calcstate, calcstate', ?Calc.T?
   13.26    \begin{itemize}
   13.27    \item by_tactic Check_Postcond' needs NO 2.find_next_step
   13.28                   solve Check_Postcond' needs, because NO prog_result in Tactic.input
   13.29 @@ -365,10 +365,10 @@
   13.30  taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
   13.31  and probably, because the Kernel interface separated setNextTactic and applyTactic.
   13.32  Both are no good reasons to make code more complicated. For instance Math_Engine.do_next
   13.33 -could drop half of the code. So try to use Ctree.state only.
   13.34 +could drop half of the code. So try to use Calc.T only.
   13.35    \begin{itemize}
   13.36    \item xxx
   13.37 -  \item Step* functions should return Ctree.state instead of Chead.calcstate'
   13.38 +  \item Step* functions should return Calc.T instead of Chead.calcstate'
   13.39    \item xxx
   13.40    \item states.sml: check, when "length tacis > 1"
   13.41    \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml