--- a/src/HOL/Real/RealDef.thy Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealDef.thy Wed Jun 07 12:14:18 2000 +0200
@@ -15,17 +15,16 @@
instance
- real :: {ord, plus, times, minus}
+ real :: {ord, zero, plus, times, minus}
consts
- "0r" :: real ("0r")
"1r" :: real ("1r")
defs
real_zero_def
- "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
+ "0 == 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) +
@@ -44,7 +43,7 @@
preal_of_prat(prat_of_pnat 1p))})"
rinv :: real => real
- "rinv(R) == (@S. R ~= 0r & S*R = 1r)"
+ "rinv(R) == (@S. R ~= 0 & S*R = 1r)"
real_of_posnat :: nat => real
"real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"