# HG changeset patch
# User nipkow
# Date 1364830949 -7200
# Node ID d40aec502416a0eaa094e5aef1f317f7c4867852
# Parent  c3a7d6592e3f209f7dfb964f46593771046b3bfe
added lemma

diff -r c3a7d6592e3f -r d40aec502416 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Mar 30 18:24:33 2013 +0100
+++ b/src/HOL/Lattices.thy	Mon Apr 01 17:42:29 2013 +0200
@@ -513,6 +513,10 @@
   "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   by (simp add: eq_iff)
 
+lemma bot_eq_sup_iff [simp]:
+  "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+  by (simp add: eq_iff)
+
 end
 
 class bounded_lattice_top = lattice + top