Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/MathEngBasic/tactic.sml
changeset 59985 9aaeab7d38b6
parent 59976 950922a768ca
child 59997 46fe5a8c3911 
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri May 15 14:22:05 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri May 15 19:31:04 2020 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
     1.5    | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
     1.6    | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
     1.7 -  | Subproblem' of References.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
     1.8 +  | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
     1.9    | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
    1.10  (*RM*)| Tac_ of theory * string * string * string
    1.11    | Take' of term
    1.12 @@ -338,7 +338,7 @@
    1.13    | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
    1.14    | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
    1.15    | Subproblem' of       (* switch from solve-phase to specify-phase         *)
    1.16 -      References.T *           (* specification of the SubProblem                  *)
    1.17 +      References_Def.T *           (* specification of the SubProblem                  *)
    1.18    		(Model_Def.o_model) * (* original model, filled in associate Subproblem'  *)
    1.19    		term *             (* headline of calc-head, filled -"-                *)
    1.20    		Model_Def.form_model *       (* string list from arguments of the calling Program*)
wneuper/isa