--- a/src/HOL/Real/RealDef.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/RealDef.thy Sat May 01 22:01:57 2004 +0200
@@ -17,13 +17,7 @@
typedef (Real) real = "UNIV//realrel"
by (auto simp add: quotient_def)
-instance real :: ord ..
-instance real :: zero ..
-instance real :: one ..
-instance real :: plus ..
-instance real :: times ..
-instance real :: minus ..
-instance real :: inverse ..
+instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
constdefs
@@ -41,6 +35,9 @@
(*overloaded constant for injecting other types into "real"*)
real :: "'a => real"
+syntax (xsymbols)
+ Reals :: "'a set" ("\<real>")
+
defs (overloaded)
@@ -83,9 +80,6 @@
real_abs_def: "abs (r::real) == (if 0 \<le> r then r else -r)"
-syntax (xsymbols)
- Reals :: "'a set" ("\<real>")
-
subsection{*Proving that realrel is an equivalence relation*}