src/Pure/simplifier.ML
changeset 17004 6a0d8ecf65f1
parent 16989 1877b00fb4d2
child 17723 ee5b42e3cbb4
     1.1 --- a/src/Pure/simplifier.ML	Tue Aug 02 19:47:13 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Tue Aug 02 19:47:14 2005 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4  signature SIMPLIFIER =
     1.5  sig
     1.6    include BASIC_SIMPLIFIER
     1.7 +  val clear_ss: simpset -> simpset
     1.8 +  val inherit_bounds: simpset -> simpset -> simpset
     1.9    val simproc_i: theory -> string -> term list
    1.10      -> (theory -> simpset -> term -> thm option) -> simproc
    1.11    val simproc: theory -> string -> string list
    1.12 @@ -60,7 +62,6 @@
    1.13      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.14    val context_simproc: theory -> string -> string list
    1.15      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.16 -  val inherit_bounds: simpset -> simpset -> simpset
    1.17    val          rewrite: simpset -> cterm -> thm
    1.18    val      asm_rewrite: simpset -> cterm -> thm
    1.19    val     full_rewrite: simpset -> cterm -> thm