1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 13 18:37:24 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Apr 14 12:39:26 2020 +0200
1.3 @@ -21,7 +21,7 @@
1.4 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.5
1.6 | CAScmd' of term
1.7 - | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
1.8 + | Calculate' of ThyC.theory' * string * term * (term * ThmC.T)
1.9 | Check_Postcond' of Celem.pblID * term
1.10 | Check_elementwise' of term * TermC.as_string * Selem.result
1.11 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
1.12 @@ -40,8 +40,8 @@
1.13 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.14 | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
1.15
1.16 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
1.17 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
1.18 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.19 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
1.20 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.21 | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.22
1.23 @@ -91,8 +91,8 @@
1.24 | Refine_Problem of Celem.pblID
1.25 | Refine_Tacitly of Celem.pblID
1.26
1.27 - | Rewrite of ThmC_Def.thm''
1.28 - | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
1.29 + | Rewrite of ThmC.T
1.30 + | Rewrite_Inst of Selem.subs * ThmC.T
1.31 | Rewrite_Set of Rule_Set.id
1.32 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
1.33
1.34 @@ -183,8 +183,8 @@
1.35 because there all the thms are present with both (thmID, thm)
1.36 (where user-views can show both or only one of (thmID, thm)),
1.37 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
1.38 - | Rewrite of ThmC_Def.thm''
1.39 - | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
1.40 + | Rewrite of ThmC.T
1.41 + | Rewrite_Inst of Selem.subs * ThmC.T
1.42 | Rewrite_Set of Rule_Set.id
1.43 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
1.44
1.45 @@ -351,7 +351,7 @@
1.46 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
1.47 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
1.48 | CAScmd' of term
1.49 - | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
1.50 + | Calculate' of ThyC.theory' * string * term * (term * ThmC.T)
1.51 | Check_Postcond' of Celem.pblID *
1.52 term (* returnvalue of program in solve *)
1.53 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
1.54 @@ -381,8 +381,8 @@
1.55 ThyC.domID * (* from new pbt?! filled in specify *)
1.56 Celem.metID * (* from new pbt?! filled in specify *)
1.57 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.58 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
1.59 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
1.60 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
1.61 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
1.62 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
1.63 | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
1.64