src/HOL/Real/RealDef.thy
changeset 9365 0cced1b20d68
parent 9043 ca761fe227d8
child 9391 a6ab3a442da6
--- 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 &