author | noschinl |
Mon, 19 Sep 2011 14:35:51 +0200 | |
changeset 44995 | eff5bccc9b76 |
parent 44994 | a915907a67d5 |
child 44996 | 410eea28b0f7 |
--- a/src/HOL/Complete_Lattices.thy Mon Sep 19 14:24:53 2011 +0200 +++ b/src/HOL/Complete_Lattices.thy Mon Sep 19 14:35:51 2011 +0200 @@ -1133,14 +1133,6 @@ text {* Legacy names *} -lemma (in complete_lattice) Inf_singleton [simp]: - "\<Sqinter>{a} = a" - by simp - -lemma (in complete_lattice) Sup_singleton [simp]: - "\<Squnion>{a} = a" - by simp - lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A" by blast