equal
deleted
inserted
replaced
6 and * (for div, mod and dvd, see theory Divides). |
6 and * (for div, mod and dvd, see theory Divides). |
7 *) |
7 *) |
8 |
8 |
9 Nat = NatDef + Inductive + |
9 Nat = NatDef + Inductive + |
10 |
10 |
11 (* type "nat" is a linear order, and a datatype *) |
11 (* type "nat" is a wellfounded linear order, and a datatype *) |
12 |
12 |
13 rep_datatype nat |
13 rep_datatype nat |
14 distinct Suc_not_Zero, Zero_not_Suc |
14 distinct Suc_not_Zero, Zero_not_Suc |
15 inject Suc_Suc_eq |
15 inject Suc_Suc_eq |
16 induct nat_induct |
16 induct nat_induct |
17 |
17 |
18 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le) |
18 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le) |
19 instance nat :: linorder (nat_le_linear) |
19 instance nat :: linorder (nat_le_linear) |
|
20 instance nat :: wellorder (wf_less) |
20 |
21 |
21 axclass power < term |
22 axclass power < term |
22 |
23 |
23 consts |
24 consts |
24 power :: ['a::power, nat] => 'a (infixr "^" 80) |
25 power :: ['a::power, nat] => 'a (infixr "^" 80) |