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 59941 602bf61dc6df
parent 59940 acfad421e656
child 59959 0f0718c61f68 
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon May 04 18:47:27 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue May 05 09:07:36 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 Spec.T * Model_Def.o_model * term * Celem.fmz_ * Proof.context * term
     1.8 +  | Subproblem' of Spec.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 @@ -341,7 +341,7 @@
    1.13        Spec.T *           (* specification of the SubProblem                  *)
    1.14    		(Model_Def.o_model) * (* original model, filled in associate Subproblem'  *)
    1.15    		term *             (* headline of calc-head, filled -"-                *)
    1.16 -  		Celem.fmz_ *       (* string list from arguments of the calling Program*)
    1.17 +  		Model_Def.form_model *       (* string list from arguments of the calling Program*)
    1.18        Proof.context *    (* for the specify-phase                            *)
    1.19    		term               (* Subproblem (thyID, pbl) OR CAS_Cmd               *)  
    1.20    | Substitute' of       (* substitute variables (TODO: from the context)    *)
wneuper/isa