equal
deleted
inserted
replaced
6 theory HOL/Numeral. |
6 theory HOL/Numeral. |
7 *) |
7 *) |
8 |
8 |
9 signature NUMERAL_SYNTAX = |
9 signature NUMERAL_SYNTAX = |
10 sig |
10 sig |
11 val setup: (theory -> theory) list |
11 val setup: theory -> theory |
12 end; |
12 end; |
13 |
13 |
14 structure NumeralSyntax: NUMERAL_SYNTAX = |
14 structure NumeralSyntax: NUMERAL_SYNTAX = |
15 struct |
15 struct |
16 |
16 |
53 |
53 |
54 |
54 |
55 (* theory setup *) |
55 (* theory setup *) |
56 |
56 |
57 val setup = |
57 val setup = |
58 [Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"], |
58 Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #> |
59 Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"], |
59 Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #> |
60 Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []), |
60 Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> |
61 Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]]; |
61 Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; |
62 |
62 |
63 end; |
63 end; |