|
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
|
|
9035
|
9 |
files "Tools/numeral_syntax.ML":
|
|
6905
|
10 |
|
|
|
11 |
datatype
|
|
|
12 |
bin = Pls
|
|
|
13 |
| Min
|
|
9035
|
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 |
|
|
|
22 |
syntax
|
|
9035
|
23 |
"_Numeral" :: "xnum => 'a" ("_")
|
|
6905
|
24 |
|
|
9035
|
25 |
setup NumeralSyntax.setup
|
|
6905
|
26 |
|
|
|
27 |
|
|
9035
|
28 |
end
|