# HG changeset patch
# User wenzelm
# Date 1154127091 -7200
# Node ID a13adb4f94dc54fe8f6bbd3a188e57c97a9e3e83
# Parent  7916ce5bb06951aad7560e4a2d6d2f99f300f8c4
added mk_conjunction_list;

diff -r 7916ce5bb069 -r a13adb4f94dc src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Sat Jul 29 00:51:29 2006 +0200
+++ b/src/Pure/conjunction.ML	Sat Jul 29 00:51:31 2006 +0200
@@ -9,6 +9,7 @@
 sig
   val conjunction: cterm
   val mk_conjunction: cterm * cterm -> cterm
+  val mk_conjunction_list: cterm list -> cterm
   val dest_conjunction: cterm -> cterm * cterm
   val cong: thm -> thm -> thm
   val conv: int -> (int -> cterm -> thm) -> cterm -> thm
@@ -37,6 +38,11 @@
 val conjunction = cert Logic.conjunction;
 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
 
+val true_prop = read "!!dummy. PROP dummy ==> PROP dummy";
+
+fun mk_conjunction_list [] = true_prop
+  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
+
 fun dest_conjunction ct =
   (case Thm.term_of ct of
     (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct