src/Pure/logic.ML
changeset 28856 5e009a80fe6d
parent 28448 31a59d7d2168
child 29276 94b1ffec9201
     1.1 --- a/src/Pure/logic.ML	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -162,33 +162,33 @@
     1.4  val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
     1.5  
     1.6  
     1.7 -(*A && B*)
     1.8 +(*A &&& B*)
     1.9  fun mk_conjunction (A, B) = conjunction $ A $ B;
    1.10  
    1.11 -(*A && B && C -- improper*)
    1.12 +(*A &&& B &&& C -- improper*)
    1.13  fun mk_conjunction_list [] = true_prop
    1.14    | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    1.15  
    1.16 -(*(A && B) && (C && D) -- balanced*)
    1.17 +(*(A &&& B) &&& (C &&& D) -- balanced*)
    1.18  fun mk_conjunction_balanced [] = true_prop
    1.19    | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
    1.20  
    1.21  
    1.22 -(*A && B*)
    1.23 +(*A &&& B*)
    1.24  fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
    1.25    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
    1.26  
    1.27 -(*A && B && C -- improper*)
    1.28 +(*A &&& B &&& C -- improper*)
    1.29  fun dest_conjunction_list t =
    1.30    (case try dest_conjunction t of
    1.31      NONE => [t]
    1.32    | SOME (A, B) => A :: dest_conjunction_list B);
    1.33  
    1.34 -(*(A && B) && (C && D) -- balanced*)
    1.35 +(*(A &&& B) &&& (C &&& D) -- balanced*)
    1.36  fun dest_conjunction_balanced 0 _ = []
    1.37    | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
    1.38  
    1.39 -(*((A && B) && C) && D && E -- flat*)
    1.40 +(*((A &&& B) &&& C) &&& D &&& E -- flat*)
    1.41  fun dest_conjunctions t =
    1.42    (case try dest_conjunction t of
    1.43      NONE => [t]