author | wenzelm |
Wed, 29 Aug 2001 21:17:24 +0200 | |
changeset 11506 | 244a02a2968b |
parent 11488 | 4ff900551340 |
child 11699 | c7df55158574 |
permissions | -rw-r--r-- |
6905 | 1 |
(* Title: HOL/Numeral.thy |
2 |
ID: $Id$ |
|
3 |
Author: Larry Paulson and Markus Wenzel |
|
4 |
||
9410
612ee826a409
removed selector syntax -- improper tuples are broken beyond repair :-(
wenzelm
parents:
9358
diff
changeset
|
5 |
Generic numerals represented as twos-complement bit strings. |
6905 | 6 |
*) |
7 |
||
8 |
theory Numeral = Datatype |
|
9035 | 9 |
files "Tools/numeral_syntax.ML": |
6905 | 10 |
|
11 |
datatype |
|
12 |
bin = Pls |
|
13 |
| Min |
|
9358
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
14 |
| Bit bin bool (infixl "BIT" 90) |
6905 | 15 |
|
16 |
axclass |
|
9035 | 17 |
number < "term" (*for numeric types: nat, int, real, ...*) |
6905 | 18 |
|
19 |
consts |
|
9035 | 20 |
number_of :: "bin => 'a::number" |
6905 | 21 |
|
11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
9410
diff
changeset
|
22 |
nonterminals |
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
9410
diff
changeset
|
23 |
numeral |
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
9410
diff
changeset
|
24 |
|
6905 | 25 |
syntax |
11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
9410
diff
changeset
|
26 |
"_constify" :: "xnum => numeral" ("_") |
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
9410
diff
changeset
|
27 |
"_Numeral" :: "numeral => 'a" ("_") |
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
9410
diff
changeset
|
28 |
|
6905 | 29 |
|
9035 | 30 |
setup NumeralSyntax.setup |
6905 | 31 |
|
9035 | 32 |
end |