--- a/src/Pure/conjunction.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/conjunction.ML Thu Nov 20 00:03:47 2008 +0100
@@ -67,7 +67,7 @@
val B = read_prop "B" and vB = read_prop "?B";
val C = read_prop "C";
val ABC = read_prop "A ==> B ==> C";
-val A_B = read_prop "A && B";
+val A_B = read_prop "A &&& B";
val conjunction_def =
Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
@@ -135,7 +135,7 @@
in
(*
- A1 && ... && An ==> B
+ A1 &&& ... &&& An ==> B
-----------------------
A1 ==> ... ==> An ==> B
*)
@@ -155,7 +155,7 @@
(*
A1 ==> ... ==> An ==> B
-----------------------
- A1 && ... && An ==> B
+ A1 &&& ... &&& An ==> B
*)
fun uncurry_balanced n th =
if n < 2 then th