equal
deleted
inserted
replaced
20 constdefs |
20 constdefs |
21 hyprel :: "((nat=>real)*(nat=>real)) set" |
21 hyprel :: "((nat=>real)*(nat=>real)) set" |
22 "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & |
22 "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & |
23 {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
23 {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
24 |
24 |
25 typedef hypreal = "{x::nat=>real. True}/hyprel" (Equiv.quotient_def) |
25 typedef hypreal = "UNIV//hyprel" (Equiv.quotient_def) |
26 |
26 |
27 instance |
27 instance |
28 hypreal :: {ord, zero, plus, times, minus} |
28 hypreal :: {ord, zero, plus, times, minus} |
29 |
29 |
30 consts |
30 consts |