src/HOL/Tools/inductive_set.ML
changeset 32306 19f55947d4d5
parent 32287 65d5c5b30747
child 32351 96f9e6402403
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Aug 04 01:01:23 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Aug 04 08:34:56 2009 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val to_set_att: thm list -> attribute
     1.6    val to_pred_att: thm list -> attribute
     1.7 +  val to_pred : thm list -> Context.generic -> thm -> thm
     1.8    val pred_set_conv_att: attribute
     1.9    val add_inductive_i:
    1.10      Inductive.inductive_flags ->