| author | paulson |
| Thu, 08 Jul 1999 13:37:40 +0200 | |
| changeset 6914 | ad689270a265 |
| parent 6905 | 9bc05ec3497b |
| child 6988 | eed63543a3af |
| permissions | -rw-r--r-- |
| 6905 | 1 |
(* Title: HOL/Numeral.thy |
2 |
ID: $Id$ |
|
3 |
Author: Larry Paulson and Markus Wenzel |
|
4 |
||
5 |
Generic numerals represented as twos-complement bitstrings. |
|
6 |
*) |
|
7 |
||
8 |
theory Numeral = Datatype |
|
9 |
files "Tools/numeral_syntax.ML":; |
|
10 |
||
11 |
datatype |
|
12 |
bin = Pls |
|
13 |
| Min |
|
14 |
| Bit bin bool (infixl "BIT" 90); |
|
15 |
||
16 |
axclass |
|
17 |
numeral < "term"; |
|
18 |
||
19 |
consts |
|
20 |
number_of :: "bin => 'a::numeral"; |
|
21 |
||
22 |
syntax |
|
23 |
"_Numeral" :: "xnum => 'a" ("_");
|
|
24 |
||
25 |
setup NumeralSyntax.setup; |
|
26 |
||
27 |
||
28 |
end; |