equal
deleted
inserted
replaced
12 val int_tr: term list -> term |
12 val int_tr: term list -> term |
13 val int_tr': bool -> typ -> term list -> term |
13 val int_tr': bool -> typ -> term list -> term |
14 val setup: theory -> theory |
14 val setup: theory -> theory |
15 end; |
15 end; |
16 |
16 |
17 structure NumeralSyntax: NUMERAL_SYNTAX = |
17 structure Numeral_Syntax: NUMERAL_SYNTAX = |
18 struct |
18 struct |
19 |
19 |
20 (* bits *) |
20 (* bits *) |
21 |
21 |
22 fun mk_bit 0 = Syntax.const @{const_syntax "0"} |
22 fun mk_bit 0 = Syntax.const @{const_syntax "0"} |