src/HOL/Real/RealDef.thy
 changeset 10606 e3229a37d53f parent 9391 a6ab3a442da6 child 10648 a8c647cfa31f
```--- a/src/HOL/Real/RealDef.thy	Wed Dec 06 12:28:52 2000 +0100
+++ b/src/HOL/Real/RealDef.thy	Wed Dec 06 12:34:12 2000 +0100
@@ -15,7 +15,7 @@

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

consts

@@ -24,17 +24,24 @@
defs

real_zero_def
-     "0 == 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) +
+  "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 (x,y):Rep_real(R). realrel^^{(y,x)})"
+  "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
+
+  real_diff_def
+  "R - (S::real) == R + - S"

-  real_diff_def "x - y == x + (- y :: real)"
+  real_inverse_def
+  "inverse (R::real) == (@S. R ~= 0 & S*R = 1r)"

+  real_divide_def
+  "R / (S::real) == R * inverse S"
+
constdefs

real_of_preal :: preal => real
@@ -42,9 +49,6 @@
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 ~= 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)))"
```