equal
deleted
inserted
replaced
233 code_syntax_const |
233 code_syntax_const |
234 Pair |
234 Pair |
235 ml (target_atom "(__,/ __)") |
235 ml (target_atom "(__,/ __)") |
236 haskell (target_atom "(__,/ __)") |
236 haskell (target_atom "(__,/ __)") |
237 |
237 |
|
238 lemma [code]: |
|
239 "fst (x, y) = x" by simp |
|
240 |
|
241 lemma [code]: |
|
242 "snd (x, y) = y" by simp |
|
243 |
238 code_syntax_const |
244 code_syntax_const |
239 1 :: "nat" |
245 1 :: "nat" |
240 ml ("{*Suc 0*}") |
246 ml ("{*Suc 0*}") |
241 haskell ("{*Suc 0*}") |
247 haskell ("{*Suc 0*}") |
242 |
248 |