| changeset 13487 | 1291c6375c29 |
| parent 12114 | a8e860c86252 |
| child 14269 | 502a7c95de73 |
--- a/src/HOL/Real/RealDef.thy Thu Aug 08 23:51:24 2002 +0200 +++ b/src/HOL/Real/RealDef.thy Thu Aug 08 23:52:55 2002 +0200 @@ -15,7 +15,7 @@ "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" typedef (REAL) - real = "UNIV//realrel" (Equiv.quotient_def) + real = "UNIV//realrel" (quotient_def) instance