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