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 59907 4c62e16e842e
parent 59901 07a042166900
child 59919 3a7fb975af9d 
     1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Apr 23 09:29:56 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Apr 23 12:34:54 2020 +0200
     1.3 @@ -9,15 +9,15 @@
     1.4    val eval_prog_expr: theory -> Rule_Set.T -> term -> term
     1.5    val eval_true_: theory -> Rule_Set.T -> term -> bool
     1.6    val eval_true: theory -> term list -> Rule_Set.T -> bool
     1.7 -  val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
     1.8 +  val rew_sub: theory -> int -> (term * term) list -> Rule_Def.rew_ord_
     1.9      -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
    1.10 -  val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
    1.11 +  val rewrite_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
    1.12      term -> (term * term list) option
    1.13 -  val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
    1.14 +  val rewrite_inst_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
    1.15      -> (term * term) list -> thm -> term -> (term * term list) option
    1.16    val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
    1.17    val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
    1.18 -  val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
    1.19 +  val rewrite_terms_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
    1.20      -> term -> (term * term list) option
    1.21  
    1.22    val trace_on: bool Unsynchronized.ref
    1.23 @@ -27,7 +27,7 @@
    1.24  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.25    (* NONE *)
    1.26  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.27 -  val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
    1.28 +  val rewrite__: theory -> int -> (term * term) list -> Rule_Def.rew_ord_ ->
    1.29      Rule_Set.T -> bool -> thm -> term -> (term * term list) option
    1.30    val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
    1.31    val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
wneuper/isa