# HG changeset patch
# User wenzelm
# Date 964954934 -7200
# Node ID 7d13a5ace928ed04e98970c8707f6f0917cf6dd5
# Parent  b63b21f370ca8b8bea6d661196068b94274aaeec
added atomic_Trueprop;

diff -r b63b21f370ca -r 7d13a5ace928 src/FOL/fologic.ML
--- 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]);
 
diff -r b63b21f370ca -r 7d13a5ace928 src/HOL/hologic.ML
--- 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]);