src/HOL/Record.thy

--- 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