equal
deleted
inserted
replaced
5 Generic numerals represented as twos-complement bit strings. |
5 Generic numerals represented as twos-complement bit strings. |
6 *) |
6 *) |
7 |
7 |
8 theory Numeral = Datatype |
8 theory Numeral = Datatype |
9 files "Tools/numeral_syntax.ML": |
9 files "Tools/numeral_syntax.ML": |
|
10 |
|
11 (* The constructors Pls/Min are hidden in numeral_syntax.ML. |
|
12 Only qualified access bin.Pls/Min is allowed. |
|
13 Should also hide Bit, but that means one cannot use BIT anymore. |
|
14 *) |
10 |
15 |
11 datatype |
16 datatype |
12 bin = Pls |
17 bin = Pls |
13 | Min |
18 | Min |
14 | Bit bin bool (infixl "BIT" 90) |
19 | Bit bin bool (infixl "BIT" 90) |
23 "_Numeral" :: "num_const => 'a" ("_") |
28 "_Numeral" :: "num_const => 'a" ("_") |
24 Numeral0 :: 'a |
29 Numeral0 :: 'a |
25 Numeral1 :: 'a |
30 Numeral1 :: 'a |
26 |
31 |
27 translations |
32 translations |
28 "Numeral0" == "number_of Pls" |
33 "Numeral0" == "number_of bin.Pls" |
29 "Numeral1" == "number_of (Pls BIT True)" |
34 "Numeral1" == "number_of (bin.Pls BIT True)" |
30 |
35 |
31 |
36 |
32 setup NumeralSyntax.setup |
37 setup NumeralSyntax.setup |
33 |
38 |
34 syntax (xsymbols) |
39 syntax (xsymbols) |