# 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 \ y = \ \ x = \ \ y = \" by (simp add: eq_iff) +lemma bot_eq_sup_iff [simp]: + "\ = x \ y \ x = \ \ y = \" + by (simp add: eq_iff) + end class bounded_lattice_top = lattice + top