Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Wed, 07 Aug 2002 20:03:38 +0200
changeset 13475 459ac22f47ff
parent 13474 f326c5d97d76
child 13476 600f1c93124f
tuned;
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/simplifier.ML	Wed Aug 07 20:03:17 2002 +0200
+++ b/src/Provers/simplifier.ML	Wed Aug 07 20:03:38 2002 +0200
@@ -16,10 +16,6 @@
   type simproc
   val mk_simproc: string -> cterm list
     -> (Sign.sg -> thm list -> term -> thm option) -> simproc
-  val simproc: Sign.sg -> string -> string list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
-  val simproc_i: Sign.sg -> string -> term list
-    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   type solver
   val mk_solver: string -> (thm list -> int -> tactic) -> solver
   type simpset
@@ -91,6 +87,10 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val simproc: Sign.sg -> string -> string list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+  val simproc_i: Sign.sg -> string -> term list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   val          rewrite: simpset -> cterm -> thm
   val      asm_rewrite: simpset -> cterm -> thm
   val     full_rewrite: simpset -> cterm -> thm
isabelle