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 59857 cbb3fae0381d
parent 59854 c20d08e01ad2
child 59861 65ec9f679c3f 
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Wed Apr 08 16:56:47 2020 +0200
     1.3 @@ -40,8 +40,8 @@
     1.4    | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
     1.5    | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
     1.6  
     1.7 -  | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
     1.8 -  | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
     1.9 +  | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
    1.10 +  | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
    1.11    | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
    1.12    | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
    1.13  
    1.14 @@ -381,8 +381,8 @@
    1.15      ThyC.domID *      (* from new pbt?! filled in specify                                     *)
    1.16      Celem.metID *     (* from new pbt?! filled in specify                                     *)
    1.17      Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
    1.18 -  | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
    1.19 -  | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
    1.20 +  | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
    1.21 +  | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
    1.22    | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
    1.23    | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
    1.24
wneuper/isa