# HG changeset patch
# User wenzelm
# Date 1002202805 -7200
# Node ID f2268239b93f6f1f8256ff328ab5f71192e2c62f
# Parent  d9063229b4a198a7149259a792f17e1e96187afa
added dest_concls;

diff -r d9063229b4a1 -r f2268239b93f src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Thu Oct 04 15:39:43 2001 +0200
+++ b/src/HOL/hologic.ML	Thu Oct 04 15:40:05 2001 +0200
@@ -28,6 +28,7 @@
   val mk_imp: term * term -> term
   val dest_imp: term -> term * term
   val dest_conj: term -> term list
+  val dest_concls: term -> term list
   val eq_const: typ -> term
   val all_const: typ -> term
   val exists_const: typ -> term
@@ -125,6 +126,9 @@
 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   | dest_conj t = [t];
 
+fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t;
+val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;
+
 fun eq_const T = Const ("op =", [T, T] ---> boolT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;