| changeset 23253 | b1f3f53c60b5 |
| parent 21404 | eb85850d3eb7 |
| child 23775 | 8b37b6615c52 |
| 23252:67268bb40b21 | 23253:b1f3f53c60b5 |
|---|---|
1 (* |
1 (* |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Makarius |
3 Author: Makarius |
4 *) |
4 *) |
5 |
5 |
6 header {* Abstract Natural Numbers with polymorphic recursion *} |
6 header {* Abstract Natural Numbers primitive recursion *} |
7 |
7 |
8 theory Abstract_NAT |
8 theory Abstract_NAT |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |