# HG changeset patch
# User wenzelm
# Date 951661334 -3600
# Node ID da404f79c1fcd4d07fafc7d3fae61605ca93628a
# Parent  d9345bad5e5ce080d892274d06942da53c52f21f
added dest_conj;

diff -r d9345bad5e5c -r da404f79c1fc src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Sun Feb 27 15:21:13 2000 +0100
+++ b/src/HOL/hologic.ML	Sun Feb 27 15:22:14 2000 +0100
@@ -25,6 +25,7 @@
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
   val dest_imp: term -> term * term
+  val dest_conj: term -> term list
   val eq_const: typ -> term
   val all_const: typ -> term
   val exists_const: typ -> term
@@ -114,6 +115,9 @@
 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
+fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+  | dest_conj t = [t];
+
 fun eq_const T = Const ("op =", [T, T] ---> boolT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;