changeset 27487 | c8a6ce181805 |
parent 27368 | 9f90ac19e32b |
child 28920 | 4ed4b8b1988d |
27486:c61507a98bff | 27487:c8a6ce181805 |
---|---|
6 *) |
6 *) |
7 |
7 |
8 header "Numeral Syntax for Types" |
8 header "Numeral Syntax for Types" |
9 |
9 |
10 theory Numeral_Type |
10 theory Numeral_Type |
11 imports Plain Presburger |
11 imports Plain "~~/src/HOL/Presburger" |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Preliminary lemmas *} |
14 subsection {* Preliminary lemmas *} |
15 (* These should be moved elsewhere *) |
15 (* These should be moved elsewhere *) |
16 |
16 |