added mk_conjunction_list;

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