# HG changeset patch
# User wenzelm
# Date 1130531282 -7200
# Node ID ab8803126f8427f492e9c088dc468dae840740a0
# Parent  3295e9982a5b57658c8bd37e1ec8ef5b9efe7437
export cong_modifiers, simp_modifiers';

diff -r 3295e9982a5b -r ab8803126f84 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