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