| changeset 51314 | eac4bb5adbf9 |
| parent 48072 | ace701efe203 |
| child 52435 | 6646bb548c6b |
| 51313:102a0a0718c5 | 51314:eac4bb5adbf9 |
|---|---|
1 (* Title: HOL/Tools/numeral.ML |
1 (* Title: HOL/Tools/numeral.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Logical operations on numerals (see also HOL/hologic.ML). |
4 Logical operations on numerals (see also HOL/Tools/hologic.ML). |
5 *) |
5 *) |
6 |
6 |
7 signature NUMERAL = |
7 signature NUMERAL = |
8 sig |
8 sig |
9 val mk_cnumeral: int -> cterm |
9 val mk_cnumeral: int -> cterm |