equal
deleted
inserted
replaced
46 context eq |
46 context eq |
47 begin |
47 begin |
48 |
48 |
49 lemma equals_eq [code inline, code func]: "op = \<equiv> eq" |
49 lemma equals_eq [code inline, code func]: "op = \<equiv> eq" |
50 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) |
50 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) |
|
51 |
|
52 declare eq [code unfold, code inline del] |
51 |
53 |
52 declare equals_eq [symmetric, code post] |
54 declare equals_eq [symmetric, code post] |
53 |
55 |
54 end |
56 end |
55 |
57 |
130 (Haskell infixl 4 "==") |
132 (Haskell infixl 4 "==") |
131 |
133 |
132 text {* undefined *} |
134 text {* undefined *} |
133 |
135 |
134 code_const undefined |
136 code_const undefined |
135 (SML "raise/ Fail/ \"undefined\"") |
137 (SML "!(raise/ Fail/ \"undefined\")") |
136 (OCaml "failwith/ \"undefined\"") |
138 (OCaml "failwith/ \"undefined\"") |
137 (Haskell "error/ \"undefined\"") |
139 (Haskell "error/ \"undefined\"") |
138 |
140 |
139 |
141 |
140 subsection {* SML code generator setup *} |
142 subsection {* SML code generator setup *} |