# HG changeset patch
# User wenzelm
# Date 1002199778 -7200
# Node ID 548ba68385a3e4cfbd13fb31df6134b8022b0ba0
# Parent  1af97cd22632d173ab6e01f472640cb5717e304a
added dest_conj, dest_concls;

diff -r 1af97cd22632 -r 548ba68385a3 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Thu Oct 04 14:49:10 2001 +0200
+++ b/src/FOL/fologic.ML	Thu Oct 04 14:49:38 2001 +0200
@@ -19,6 +19,8 @@
   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 dest_concls       : term -> term list
   val mk_iff		: term * term -> term
   val dest_iff	       	: term -> term*term
   val all_const		: typ -> term
@@ -62,6 +64,12 @@
 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 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 dest_iff (Const("op <->",_) $ A $ B) = (A, B)
   | dest_iff  t = raise TERM ("dest_iff", [t]);