--- a/src/FOL/fologic.ML Sun Jul 30 13:01:50 2000 +0200
+++ b/src/FOL/fologic.ML Sun Jul 30 13:02:14 2000 +0200
@@ -9,6 +9,7 @@
sig
val oT : typ
val mk_Trueprop : term -> term
+ val atomic_Trueprop : string -> term
val dest_Trueprop : term -> term
val conj : term
val disj : term
@@ -36,6 +37,8 @@
fun mk_Trueprop P = Trueprop $ P;
+fun atomic_Trueprop x = mk_Trueprop (Free (x, oT));
+
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
--- 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]);