changeset 32764 | 690f9cccf232 |
parent 32763 | ebfaf9e3c03a |
child 32799 | 7478ea535416 |
--- a/src/HOL/Record.thy Tue Sep 29 21:36:49 2009 +0200 +++ b/src/HOL/Record.thy Tue Sep 29 22:33:27 2009 +0200 @@ -18,10 +18,6 @@ lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" by (simp add: comp_def) -lemma meta_iffD2: - "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P" - by simp - lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v" by clarsimp