--- a/src/HOL/Tools/hologic.ML Sat Sep 10 10:29:24 2011 +0200
+++ b/src/HOL/Tools/hologic.ML Sat Sep 10 19:44:41 2011 +0200
@@ -17,6 +17,7 @@
val dest_Trueprop: term -> term
val true_const: term
val false_const: term
+ val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
val Collect_const: typ -> term
@@ -164,6 +165,8 @@
val true_const = Const ("HOL.True", boolT);
val false_const = Const ("HOL.False", boolT);
+fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
+
fun mk_setT T = T --> boolT;
fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T