src/HOL/Real/RealDef.thy
 changeset 11713 883d559b0b8c parent 11701 3d51fbf81c17 child 12018 ec054019c910
```--- a/src/HOL/Real/RealDef.thy	Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon Oct 08 15:23:20 2001 +0200
@@ -19,11 +19,9 @@

instance
-   real  :: {ord, zero, plus, times, minus, inverse}
+   real  :: {ord, zero, one, plus, times, minus, inverse}

consts
-  "1r"   :: real               ("1r")
-
(*Overloaded constants denoting the Nat and Real subsets of enclosing
types such as hypreal and complex*)
Nats, Reals :: "'a set"
@@ -38,7 +36,7 @@
"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) +
+  "1 == 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
@@ -48,7 +46,7 @@
"R - (S::real) == R + - S"

real_inverse_def
-  "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1r)"
+  "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"

real_divide_def
"R / (S::real) == R * inverse S"
@@ -69,7 +67,7 @@
defs