# HG changeset patch # User wenzelm # Date 1122916843 -7200 # Node ID 1877b00fb4d2046b3805a2dfb4813b98102dacce # Parent 02cd0c8b96d91b0fef7c7bf3f2403b2ad8925b95 export MataSimplifier.inherit_bounds; diff -r 02cd0c8b96d9 -r 1877b00fb4d2 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Mon Aug 01 19:20:42 2005 +0200 +++ b/src/Pure/simplifier.ML Mon Aug 01 19:20:43 2005 +0200 @@ -60,6 +60,7 @@ -> (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