src/HOL/Real/RealDef.thy
changeset 9391 a6ab3a442da6
parent 9365 0cced1b20d68
child 10606 e3229a37d53f
--- a/src/HOL/Real/RealDef.thy	Wed Jul 19 12:28:32 2000 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jul 19 12:33:19 2000 +0200
@@ -11,7 +11,7 @@
   realrel   ::  "((preal * preal) * (preal * preal)) set"
   "realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
 
-typedef real = "{x::(preal*preal).True}/realrel"          (Equiv.quotient_def)
+typedef real = "UNIV//realrel"  (Equiv.quotient_def)
 
 
 instance