equal
deleted
inserted
replaced
6 |
6 |
7 theory Code_Generator |
7 theory Code_Generator |
8 imports HOL |
8 imports HOL |
9 begin |
9 begin |
10 |
10 |
11 subsection {* ML code generator *} |
11 subsection {* SML code generator setup *} |
12 |
12 |
13 types_code |
13 types_code |
14 "bool" ("bool") |
14 "bool" ("bool") |
15 attach (term_of) {* |
15 attach (term_of) {* |
16 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
16 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
73 |
73 |
74 subsection {* Generic code generator setup *} |
74 subsection {* Generic code generator setup *} |
75 |
75 |
76 text {* operational equality for code generation *} |
76 text {* operational equality for code generation *} |
77 |
77 |
78 axclass eq \<subseteq> type |
78 class eq (attach "op =") = notes reflexive |
79 (attach "op =") |
|
80 |
79 |
81 |
80 |
82 text {* equality for Haskell *} |
81 text {* equality for Haskell *} |
83 |
82 |
84 code_class eq |
83 code_class eq |