--- 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;