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/rewrite.sml
changeset 60477 4ac966aaa785
parent 60390 569ade776d59
child 60500 59a3af532717 
     1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 21 13:51:04 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 21 16:04:43 2022 +0200
     1.3 @@ -6,18 +6,18 @@
     1.4  sig
     1.5    exception NO_REWRITE
     1.6    val calculate_: theory -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
     1.7 -  val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
     1.8 +  val eval__true: theory -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool
     1.9    val eval_prog_expr: theory -> Rule_Set.T -> term -> term
    1.10    val eval_true_: theory -> Rule_Set.T -> term -> bool
    1.11    val eval_true: theory -> term list -> Rule_Set.T -> bool
    1.12 -  val rew_sub: theory -> int -> (term * term) list -> Rule_Def.rew_ord_
    1.13 +  val rew_sub: theory -> int -> Subst.T -> Rule_Def.rew_ord_
    1.14      -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
    1.15    val rewrite_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
    1.16      term -> (term * term list) option
    1.17    val rewrite_inst_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
    1.18 -    -> (term * term) list -> thm -> term -> (term * term list) option
    1.19 +    -> Subst.T -> thm -> term -> (term * term list) option
    1.20    val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
    1.21 -  val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
    1.22 +  val rewrite_set_inst_: theory -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
    1.23    val rewrite_terms_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
    1.24      -> term -> (term * term list) option
    1.25  
    1.26 @@ -26,9 +26,9 @@
    1.27    val lim_deriv: int Unsynchronized.ref
    1.28  
    1.29  \<^isac_test>\<open>
    1.30 -  val rewrite__: theory -> int -> (term * term) list -> Rule_Def.rew_ord_ ->
    1.31 +  val rewrite__: theory -> int -> Subst.T -> Rule_Def.rew_ord_ ->
    1.32      Rule_Set.T -> bool -> thm -> term -> (term * term list) option
    1.33 -  val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
    1.34 +  val rewrite__set_: theory -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
    1.35    val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
    1.36    val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
    1.37    val trace1: int -> string -> unit
wneuper/isa