equal
deleted
inserted
replaced
23 {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
23 {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
24 |
24 |
25 typedef hypreal = "UNIV//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, inverse} |
28 hypreal :: {ord, zero, one, plus, times, minus, inverse} |
29 |
|
30 consts |
|
31 |
|
32 "1hr" :: hypreal ("1hr") |
|
33 |
|
34 |
29 |
35 defs |
30 defs |
36 |
31 |
37 hypreal_zero_def |
32 hypreal_zero_def |
38 "0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})" |
33 "0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})" |
39 |
34 |
40 hypreal_one_def |
35 hypreal_one_def |
41 "1hr == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})" |
36 "1 == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})" |
42 |
37 |
43 hypreal_minus_def |
38 hypreal_minus_def |
44 "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" |
39 "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" |
45 |
40 |
46 hypreal_diff_def |
41 hypreal_diff_def |