| changeset 27487 | c8a6ce181805 |
| parent 27368 | 9f90ac19e32b |
| child 27823 | 52971512d1a2 |
| 27486:c61507a98bff | 27487:c8a6ce181805 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Natural numbers with infinity *} |
6 header {* Natural numbers with infinity *} |
7 |
7 |
8 theory Nat_Infinity |
8 theory Nat_Infinity |
9 imports Plain Presburger |
9 imports Plain "~~/src/HOL/Presburger" |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Type definition *} |
12 subsection {* Type definition *} |
13 |
13 |
14 text {* |
14 text {* |