--- a/src/HOL/Integ/Equiv.ML Sun Jul 16 20:55:17 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML Sun Jul 16 20:55:56 2000 +0200
@@ -209,7 +209,7 @@
(*Allows a natural expression of binary operators, without explicit calls
to "split"*)
Goal "(UN (x1,x2):X. UN (y1,y2):Y. A x1 x2 y1 y2) = \
-\ (UN x:X. UN y:Y. split(%x1 x2. split(%y1 y2. A x1 x2 y1 y2) y) x)";
+\ (UN x:X. UN y:Y. (%(x1, x2). (%(y1, y2). A x1 x2 y1 y2) y) x)";
by Auto_tac;
qed "UN_UN_split_split_eq";
--- a/src/HOL/Real/RealDef.thy Sun Jul 16 20:55:17 2000 +0200
+++ b/src/HOL/Real/RealDef.thy Sun Jul 16 20:55:56 2000 +0200
@@ -55,11 +55,11 @@
real_add_def
"P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
- split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"
+ (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
real_mult_def
"P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
- split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
+ (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
real_less_def
"P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 &
--- a/src/HOL/Real/RealInt.ML Sun Jul 16 20:55:17 2000 +0200
+++ b/src/HOL/Real/RealInt.ML Sun Jul 16 20:55:56 2000 +0200
@@ -7,7 +7,7 @@
Goalw [congruent_def]
- "congruent intrel (%p. split (%i j. realrel ^^ \
+ "congruent intrel (%p. (%(i,j). realrel ^^ \
\ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \
\ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)";
by (auto_tac (claset(),