--- a/src/HOL/Complete_Lattice.thy Mon Jul 18 18:52:52 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Mon Jul 18 21:15:51 2011 +0200
@@ -397,14 +397,6 @@
shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
unfolding SUP_def less_Sup_iff by auto
--- "FIXME move"
-
-lemma image_ident [simp]: "(%x. x) ` Y = Y"
- by blast
-
-lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
- by blast
-
class complete_boolean_algebra = boolean_algebra + complete_lattice
begin