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.
export clear_ss;
authorwenzelm
Tue, 02 Aug 2005 19:47:14 +0200
changeset 17004 6a0d8ecf65f1
parent 17003 b902e11b3df1
child 17005 69c415d44883
export clear_ss;
src/Pure/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/simplifier.ML	Tue Aug 02 19:47:13 2005 +0200
+++ b/src/Pure/simplifier.ML	Tue Aug 02 19:47:14 2005 +0200
@@ -52,6 +52,8 @@
 signature SIMPLIFIER =
 sig
   include BASIC_SIMPLIFIER
+  val clear_ss: simpset -> simpset
+  val inherit_bounds: simpset -> simpset -> simpset
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
@@ -60,7 +62,6 @@
     -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
   val context_simproc: theory -> string -> string list
     -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
-  val inherit_bounds: simpset -> simpset -> simpset
   val          rewrite: simpset -> cterm -> thm
   val      asm_rewrite: simpset -> cterm -> thm
   val     full_rewrite: simpset -> cterm -> thm
isabelle