changeset 29629 | 5111ce425e7a |
parent 29025 | 8c8859c0d734 |
child 29997 | f6756c097c2d |
child 30240 | 5b25fee0362c |
29628:d9294387ab0e | 29629:5111ce425e7a |
---|---|
1 (* |
1 (* Title: HOL/Library/Numeral_Type.thy |
2 ID: $Id$ |
2 Author: Brian Huffman |
3 Author: Brian Huffman |
|
4 |
|
5 Numeral Syntax for Types |
|
6 *) |
3 *) |
7 |
4 |
8 header "Numeral Syntax for Types" |
5 header {* Numeral Syntax for Types *} |
9 |
6 |
10 theory Numeral_Type |
7 theory Numeral_Type |
11 imports Plain "~~/src/HOL/Presburger" |
8 imports Plain "~~/src/HOL/Presburger" |
12 begin |
9 begin |
13 |
10 |