src/Pure/simplifier.ML
changeset 16989 1877b00fb4d2
parent 16806 916387f7afd2
child 17004 6a0d8ecf65f1
     1.1 --- a/src/Pure/simplifier.ML	Mon Aug 01 19:20:42 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Mon Aug 01 19:20:43 2005 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
     1.5    val context_simproc: theory -> string -> string list
     1.6      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
     1.7 +  val inherit_bounds: simpset -> simpset -> simpset
     1.8    val          rewrite: simpset -> cterm -> thm
     1.9    val      asm_rewrite: simpset -> cterm -> thm
    1.10    val     full_rewrite: simpset -> cterm -> thm