--- a/src/HOL/hologic.ML Sun Jul 30 13:01:50 2000 +0200
+++ b/src/HOL/hologic.ML Sun Jul 30 13:02:14 2000 +0200
@@ -17,6 +17,7 @@
val mk_setT: typ -> typ
val dest_setT: typ -> typ
val mk_Trueprop: term -> term
+ val atomic_Trueprop: string -> term
val dest_Trueprop: term -> term
val conj: term
val disj: term
@@ -103,6 +104,8 @@
fun mk_Trueprop P = Trueprop $ P;
+fun atomic_Trueprop x = mk_Trueprop (Free (x, boolT));
+
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);