1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat Apr 04 12:11:32 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 06 11:44:36 2020 +0200
1.3 @@ -26,9 +26,9 @@
1.4 | Check_elementwise' of term * Rule.cterm' * Selem.result
1.5 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.6
1.7 - | Derive' of Rule_Set.rls
1.8 - | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.9 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.10 + | Derive' of Rule_Set.T
1.11 + | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.12 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.13 | End_Detail' of Selem.result
1.14
1.15 | Empty_Tac_
1.16 @@ -40,10 +40,10 @@
1.17 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
1.18 | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
1.19
1.20 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
1.21 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.22 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.23 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.24 + | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.25 + | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.26 + | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.27 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.28
1.29 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.30 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
1.31 @@ -55,7 +55,7 @@
1.32 (*Istate.T * ? *)
1.33 Proof.context * (* derived from prog. in ??? *)
1.34 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
1.35 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.rls * Selem.subte * term * term
1.36 + | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Selem.subte * term * term
1.37 | Tac_ of theory * string * string * string
1.38 | Take' of term
1.39 val string_of: T -> string
1.40 @@ -360,9 +360,9 @@
1.41 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
1.42 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
1.43
1.44 - | Derive' of Rule_Set.rls
1.45 - | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.46 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.47 + | Derive' of Rule_Set.T
1.48 + | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.49 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.50 | End_Detail' of Selem.result
1.51
1.52 | Empty_Tac_
1.53 @@ -381,10 +381,10 @@
1.54 Rule.domID * (* from new pbt?! filled in specify *)
1.55 Celem.metID * (* from new pbt?! filled in specify *)
1.56 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
1.57 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
1.58 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.59 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
1.60 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
1.61 + | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
1.62 + | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
1.63 + | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
1.64 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
1.65
1.66 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
1.67 | Specify_Problem' of Celem.pblID *
1.68 @@ -401,7 +401,7 @@
1.69 term (* Subproblem (thyID, pbl) OR cascmd *)
1.70 | Substitute' of
1.71 Rule_Def.rew_ord_ * (* for re-calculation *)
1.72 - Rule_Set.rls * (* for re-calculation *)
1.73 + Rule_Set.T * (* for re-calculation *)
1.74 Selem.subte * (* the 'substitution': terms of type bool *)
1.75 term * (* to be substituted into *)
1.76 term (* resulting from the substitution *)