--- a/src/HOL/hologic.ML Mon Oct 02 17:32:18 2006 +0200
+++ b/src/HOL/hologic.ML Mon Oct 02 17:33:13 2006 +0200
@@ -17,6 +17,7 @@
val dest_setT: typ -> typ
val Trueprop: term
val mk_Trueprop: term -> term
+ val is_Trueprop: term -> bool
val dest_Trueprop: term -> term
val conj: term
val disj: term
@@ -119,6 +120,9 @@
fun mk_Trueprop P = Trueprop $ P;
+fun is_Trueprop (Const ("Trueprop", _) $ _) = true
+ | is_Trueprop t = false;
+
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);