# HG changeset patch
# User paulson
# Date 1159803193 -7200
# Node ID e3a503048f9bb204d9edc844625a35af7266fc62
# Parent  32640c8956e70a5b681c331c9d6f6b796976aac5
added is_Trueprop

diff -r 32640c8956e7 -r e3a503048f9b src/HOL/hologic.ML
--- 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]);