# HG changeset patch
# User haftmann
# Date 1164631366 -3600
# Node ID 7cc49399929a17a3c0b779f4207740e86cfdaa62
# Parent  12eff58b56a03a0deb4e48298486131790fed79e
added Trueprop_conv

diff -r 12eff58b56a0 -r 7cc49399929a src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon Nov 27 13:42:42 2006 +0100
+++ b/src/HOL/hologic.ML	Mon Nov 27 13:42:46 2006 +0100
@@ -18,6 +18,7 @@
   val Trueprop: term
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
+  val Trueprop_conv: (cterm -> thm) -> cterm -> thm
   val conj: term
   val disj: term
   val imp: term
@@ -131,6 +132,11 @@
 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
+fun Trueprop_conv conv ct = (case term_of ct of
+    Const ("Trueprop", _) $ _ =>
+      let val (ct1, ct2) = Thm.dest_comb ct
+      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
+  | _ => raise TERM ("Trueprop_conv", []));
 
 val conj = Const ("op &", [boolT, boolT] ---> boolT)
 and disj = Const ("op |", [boolT, boolT] ---> boolT)