src/Pure/logic.ML
changeset 19125 59b26248547b
parent 19103 0eb600479944
child 19391 4812d28c90a6
     1.1 --- a/src/Pure/logic.ML	Wed Feb 22 22:18:38 2006 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Feb 22 22:18:39 2006 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val strip_prems: int * term list * term -> term list * term
     1.5    val count_prems: term * int -> int
     1.6    val nth_prem: int * term -> term
     1.7 +  val conjunction: term
     1.8    val mk_conjunction: term * term -> term
     1.9    val mk_conjunction_list: term list -> term
    1.10    val mk_conjunction_list2: term list list -> term
    1.11 @@ -144,10 +145,10 @@
    1.12  
    1.13  (** conjunction **)
    1.14  
    1.15 +val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
    1.16 +
    1.17  (*A && B*)
    1.18 -fun mk_conjunction (t, u) =
    1.19 -  Term.list_all ([("X", propT)],
    1.20 -    mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0));
    1.21 +fun mk_conjunction (A, B) = conjunction $ A $ B;
    1.22  
    1.23  (*A && B && C -- improper*)
    1.24  fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
    1.25 @@ -158,12 +159,7 @@
    1.26    mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
    1.27  
    1.28  (*A && B*)
    1.29 -fun dest_conjunction
    1.30 -      (t as Const ("all", _) $ Abs (_, _,
    1.31 -        Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) =
    1.32 -      if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0)
    1.33 -      then raise TERM ("dest_conjunction", [t])
    1.34 -      else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B)
    1.35 +fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
    1.36    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
    1.37  
    1.38  (*((A && B) && C) && D && E -- flat*)