added mk_conjunction_list;
authorwenzelm
Sat Jul 29 00:51:31 2006 +0200 (2006-07-29)
changeset 20249a13adb4f94dc
parent 20248 7916ce5bb069
child 20250 c3f209752749
added mk_conjunction_list;
src/Pure/conjunction.ML
     1.1 --- a/src/Pure/conjunction.ML	Sat Jul 29 00:51:29 2006 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Sat Jul 29 00:51:31 2006 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val conjunction: cterm
     1.6    val mk_conjunction: cterm * cterm -> cterm
     1.7 +  val mk_conjunction_list: cterm list -> cterm
     1.8    val dest_conjunction: cterm -> cterm * cterm
     1.9    val cong: thm -> thm -> thm
    1.10    val conv: int -> (int -> cterm -> thm) -> cterm -> thm
    1.11 @@ -37,6 +38,11 @@
    1.12  val conjunction = cert Logic.conjunction;
    1.13  fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    1.14  
    1.15 +val true_prop = read "!!dummy. PROP dummy ==> PROP dummy";
    1.16 +
    1.17 +fun mk_conjunction_list [] = true_prop
    1.18 +  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    1.19 +
    1.20  fun dest_conjunction ct =
    1.21    (case Thm.term_of ct of
    1.22      (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct