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 59737 5e2834f8a655
parent 59736 2d7ca75b32f7
child 59740 5b8b3475d5a6 
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Dec 16 15:56:20 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue Dec 17 16:31:46 2019 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4      Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list 
     1.5    | Add_Relation' of Rule.cterm' * Model.itm list
     1.6    | Apply_Assumption' of term list * term
     1.7 -  | Apply_Method' of Celem.metID * term option * Istate.T * Proof.context
     1.8 +  | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
     1.9  
    1.10    | Begin_Sequ' | Begin_Trans' of term
    1.11    | Split_And' of term | Split_Or' of term | Split_Intersect' of term
    1.12 @@ -335,7 +335,7 @@
    1.13      Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list 
    1.14    | Add_Relation' of Rule.cterm' * Model.itm list
    1.15    | Apply_Assumption' of term list * term
    1.16 -  | Apply_Method' of Celem.metID * term option * Istate.T * Proof.context
    1.17 +  | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
    1.18    (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
    1.19    | Begin_Sequ' | Begin_Trans' of term
    1.20    | Split_And' of term | Split_Or' of term | Split_Intersect' of term
wneuper/isa