# HG changeset patch
# User haftmann
# Date 1312824618 -7200
# Node ID 9f8790f8e589d108da50cbf7cebee4fd531b8208
# Parent  81e55342cb86251b7b9bbe1919cd7637fce8c69c
dropped lemmas (Inf|Sup)_(singleton|binary)

diff -r 81e55342cb86 -r 9f8790f8e589 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Aug 08 19:21:11 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Mon Aug 08 19:30:18 2011 +0200
@@ -284,7 +284,7 @@
   proof
     assume "\<forall>x\<in>A. x = \<top>"
     then have "A = {} \<or> A = {\<top>}" by auto
-    then show "\<Sqinter>A = \<top>" by auto
+    then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
   next
     assume "\<Sqinter>A = \<top>"
     show "\<forall>x\<in>A. x = \<top>"
@@ -1190,19 +1190,19 @@
 
 text {* Legacy names *}
 
-lemma Inf_singleton [simp]:
+lemma (in complete_lattice) Inf_singleton [simp]:
   "\<Sqinter>{a} = a"
-  by (auto intro: antisym Inf_lower Inf_greatest)
+  by (simp add: Inf_insert)
 
-lemma Sup_singleton [simp]:
+lemma (in complete_lattice) Sup_singleton [simp]:
   "\<Squnion>{a} = a"
-  by (auto intro: antisym Sup_upper Sup_least)
+  by (simp add: Sup_insert)
 
-lemma Inf_binary:
+lemma (in complete_lattice) Inf_binary:
   "\<Sqinter>{a, b} = a \<sqinter> b"
   by (simp add: Inf_insert)
 
-lemma Sup_binary:
+lemma (in complete_lattice) Sup_binary:
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_insert)