| changeset 8856 | 435187ffc64e |
| parent 7562 | 8519d5019309 |
| child 10834 | a7897aebbffc |
| 8855:ef4848bb0696 | 8856:435187ffc64e |
|---|---|
4 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
5 Description : The positive naturals |
5 Description : The positive naturals |
6 *) |
6 *) |
7 |
7 |
8 |
8 |
9 PNat = Arith + |
9 PNat = Main + |
10 |
10 |
11 typedef |
11 typedef |
12 pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def) |
12 pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def) |
13 |
13 |
14 instance |
14 instance |