| changeset 55066 | 4e5ddf3162ac |
| parent 54147 | 97a8ff4e4ac9 |
| child 56047 | 1f283d0a4966 |
--- a/src/HOL/Record.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Record.thy Mon Jan 20 18:24:56 2014 +0100 @@ -411,12 +411,6 @@ lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" by (simp add: comp_def) -lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v" - by clarsimp - -lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v" - by clarsimp - subsection {* Concrete record syntax *}