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 59910 778899c624a6
parent 59903 5037ca1b112b
child 59911 ff30cec13f4f 
     1.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 24 08:51:05 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Apr 24 09:01:48 2020 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5    | Derive' of Rule_Set.T      
     1.6    | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
     1.7 -  | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
     1.8 +  | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
     1.9    | End_Detail' of Selem.result
    1.10  
    1.11    | Empty_Tac_
    1.12 @@ -41,9 +41,9 @@
    1.13    | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
    1.14  
    1.15    | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
    1.16 -  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
    1.17 +  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
    1.18    | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
    1.19 -  | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
    1.20 +  | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
    1.21  
    1.22    | Specify_Method' of Method.id * Model.ori list * Model.itm list
    1.23    | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
    1.24 @@ -362,7 +362,7 @@
    1.25  
    1.26    | Derive' of Rule_Set.T
    1.27    | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
    1.28 -  | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
    1.29 +  | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
    1.30    | End_Detail' of Selem.result
    1.31  
    1.32    | Empty_Tac_
    1.33 @@ -382,9 +382,9 @@
    1.34      Method.id *     (* from new pbt?! filled in specify                                     *)
    1.35      Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
    1.36    | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
    1.37 -  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
    1.38 +  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
    1.39    | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
    1.40 -  | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
    1.41 +  | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
    1.42  
    1.43    | Specify_Method' of Method.id * Model.ori list * Model.itm list
    1.44    | Specify_Problem' of Problem.id *
wneuper/isa