# HG changeset patch
# User noschinl
# Date 1316435751 -7200
# Node ID eff5bccc9b76beb1b9bf1ef71962fb47c7c07ca8
# Parent  a915907a67d55762cf3052375bd90f41fbe830c5
removed legacy lemmas in Complete_Lattices

diff -r a915907a67d5 -r eff5bccc9b76 src/HOL/Complete_Lattices.thy
--- 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