changeset 9391 | a6ab3a442da6 |
parent 9055 | f020e00c6304 |
child 10568 | a7701b1d6c6a |
--- a/src/HOL/Real/Hyperreal/HyperDef.thy Wed Jul 19 12:28:32 2000 +0200 +++ b/src/HOL/Real/Hyperreal/HyperDef.thy Wed Jul 19 12:33:19 2000 +0200 @@ -22,7 +22,7 @@ "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" -typedef hypreal = "{x::nat=>real. True}/hyprel" (Equiv.quotient_def) +typedef hypreal = "UNIV//hyprel" (Equiv.quotient_def) instance hypreal :: {ord, zero, plus, times, minus}