src/HOL/Lattices.thy
changeset 51593 d40aec502416
parent 51546 2e26df807dc7
child 52152 b561cdce6c4c
     1.1 --- a/src/HOL/Lattices.thy	Sat Mar 30 18:24:33 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Mon Apr 01 17:42:29 2013 +0200
     1.3 @@ -513,6 +513,10 @@
     1.4    "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
     1.5    by (simp add: eq_iff)
     1.6  
     1.7 +lemma bot_eq_sup_iff [simp]:
     1.8 +  "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
     1.9 +  by (simp add: eq_iff)
    1.10 +
    1.11  end
    1.12  
    1.13  class bounded_lattice_top = lattice + top