export cong_modifiers, simp_modifiers';
authorwenzelm
Fri, 28 Oct 2005 22:28:02 +0200
changeset 18033 ab8803126f84
parent 18032 3295e9982a5b
child 18034 5351a1538ea5
export cong_modifiers, simp_modifiers';
src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Oct 28 22:28:00 2005 +0200
+++ b/src/Pure/simplifier.ML	Fri Oct 28 22:28:02 2005 +0200
@@ -74,6 +74,8 @@
   val cong_del_global: theory attribute
   val cong_add_local: Proof.context attribute
   val cong_del_local: Proof.context attribute
+  val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
+  val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
     -> (theory -> theory) list