| changeset 10891 | 890b117f6189 |
| parent 10693 | 9e4a0e84d0d6 |
| child 11488 | 4ff900551340 |
| 10890:0b4e916f51ed | 10891:890b117f6189 |
|---|---|
7 theory HOL/Numeral. |
7 theory HOL/Numeral. |
8 *) |
8 *) |
9 |
9 |
10 signature NUMERAL_SYNTAX = |
10 signature NUMERAL_SYNTAX = |
11 sig |
11 sig |
12 val dest_bin : term -> int |
12 val setup: (theory -> theory) list |
13 val setup : (theory -> theory) list |
|
14 end; |
13 end; |
15 |
14 |
16 structure NumeralSyntax: NUMERAL_SYNTAX = |
15 structure NumeralSyntax: NUMERAL_SYNTAX = |
17 struct |
16 struct |
18 |
17 |