# HG changeset patch
# User wenzelm
# Date 963773756 -7200
# Node ID 0cced1b20d685bdb1f0e8438f80fbf9875699ffa
# Parent  e783491b9a1f43c33664d3578e37b373e1d38eb6
use split syntax;

diff -r e783491b9a1f -r 0cced1b20d68 src/HOL/Integ/Equiv.ML
--- 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";
 
diff -r e783491b9a1f -r 0cced1b20d68 src/HOL/Real/RealDef.thy
--- 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 & 
diff -r e783491b9a1f -r 0cced1b20d68 src/HOL/Real/RealInt.ML
--- 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(),