equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Binary Numerals *} |
6 header {* Binary Numerals *} |
7 |
7 |
8 theory Num |
8 theory Num |
9 imports Datatype |
9 imports Datatype BNF_LFP |
10 begin |
10 begin |
11 |
11 |
12 subsection {* The @{text num} type *} |
12 subsection {* The @{text num} type *} |
13 |
13 |
14 datatype num = One | Bit0 num | Bit1 num |
14 datatype num = One | Bit0 num | Bit1 num |
1247 |
1247 |
1248 code_identifier |
1248 code_identifier |
1249 code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
1249 code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
1250 |
1250 |
1251 end |
1251 end |
1252 |
|