equal
deleted
inserted
replaced
409 by simp |
409 by simp |
410 |
410 |
411 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
411 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
412 by (simp add: comp_def) |
412 by (simp add: comp_def) |
413 |
413 |
414 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v" |
|
415 by clarsimp |
|
416 |
|
417 lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v" |
|
418 by clarsimp |
|
419 |
|
420 |
414 |
421 subsection {* Concrete record syntax *} |
415 subsection {* Concrete record syntax *} |
422 |
416 |
423 nonterminal |
417 nonterminal |
424 ident and |
418 ident and |