equal
deleted
inserted
replaced
5 |
5 |
6 header {* Binary Numerals *} |
6 header {* Binary Numerals *} |
7 |
7 |
8 theory Num |
8 theory Num |
9 imports Datatype |
9 imports Datatype |
10 uses |
|
11 ("Tools/numeral.ML") |
|
12 begin |
10 begin |
13 |
11 |
14 subsection {* The @{text num} type *} |
12 subsection {* The @{text num} type *} |
15 |
13 |
16 datatype num = One | Bit0 num | Bit1 num |
14 datatype num = One | Bit0 num | Bit1 num |
331 end; |
329 end; |
332 in [(@{const_syntax numeral}, num_tr' ""), |
330 in [(@{const_syntax numeral}, num_tr' ""), |
333 (@{const_syntax neg_numeral}, num_tr' "-")] end |
331 (@{const_syntax neg_numeral}, num_tr' "-")] end |
334 *} |
332 *} |
335 |
333 |
336 use "Tools/numeral.ML" |
334 ML_file "Tools/numeral.ML" |
337 |
335 |
338 |
336 |
339 subsection {* Class-specific numeral rules *} |
337 subsection {* Class-specific numeral rules *} |
340 |
338 |
341 text {* |
339 text {* |