equal
deleted
inserted
replaced
15 {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
15 {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" |
16 |
16 |
17 typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel" |
17 typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel" |
18 by (auto simp add: quotient_def) |
18 by (auto simp add: quotient_def) |
19 |
19 |
20 instance hcomplex :: zero .. |
20 instance hcomplex :: "{zero, one, plus, times, minus, inverse, power}" .. |
21 instance hcomplex :: one .. |
|
22 instance hcomplex :: plus .. |
|
23 instance hcomplex :: times .. |
|
24 instance hcomplex :: minus .. |
|
25 instance hcomplex :: inverse .. |
|
26 instance hcomplex :: power .. |
|
27 |
21 |
28 defs (overloaded) |
22 defs (overloaded) |
29 hcomplex_zero_def: |
23 hcomplex_zero_def: |
30 "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})" |
24 "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})" |
31 |
25 |