src/HOL/Real/RealDef.thy
changeset 7077 60b098bb8b8a
parent 5787 4e5c74b7cd9e
child 7127 48e235179ffb
--- a/src/HOL/Real/RealDef.thy	Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/RealDef.thy	Fri Jul 23 17:29:12 1999 +0200
@@ -23,24 +23,33 @@
 
 defs
 
-  real_zero_def  "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})"
-  real_one_def   "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})"
+  real_zero_def  
+     "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
+                                preal_of_prat(prat_of_pnat 1p))})"
+  real_one_def   
+     "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
+            preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
 
   real_minus_def
-    "- R ==  Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)"
+    "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
 
   real_diff_def "x - y == x + -(y::real)"
 
 constdefs
 
-  real_preal :: preal => real              ("%#_" [100] 100)
-  "%# m     == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
+  real_of_preal :: preal => real            
+  "real_of_preal m     ==
+           Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p),
+                               preal_of_prat(prat_of_pnat 1p))})"
 
   rinv       :: real => real
   "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
 
-  real_nat :: nat => real                  ("%%# _" [100] 100) 
-  "%%# n      == %#(@#($#(*# n)))"
+  real_of_posnat :: nat => real             
+  "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
+
+  real_of_nat :: nat => real          
+  "real_of_nat n    == real_of_posnat n + -1r"
 
 defs