equal
deleted
inserted
replaced
12 |
12 |
13 text {* |
13 text {* |
14 Arithmetic for naturals is reduced to that for the non-negative integers. |
14 Arithmetic for naturals is reduced to that for the non-negative integers. |
15 *} |
15 *} |
16 |
16 |
17 instance nat :: number .. |
17 instance nat :: number |
18 |
18 nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))" .. |
19 defs (overloaded) |
|
20 nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))" |
|
21 |
19 |
22 abbreviation (xsymbols) |
20 abbreviation (xsymbols) |
23 square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where |
21 square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where |
24 "x\<twosuperior> == x^2" |
22 "x\<twosuperior> == x^2" |
25 |
23 |