# HG changeset patch # User wenzelm # Date 1123004834 -7200 # Node ID 6a0d8ecf65f10dd6fc531abc4824e29cf0155426 # Parent b902e11b3df1319513c301815903e5925606d678 export clear_ss; diff -r b902e11b3df1 -r 6a0d8ecf65f1 src/Pure/simplifier.ML --- 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