added lemma
authornipkow
Mon Apr 01 17:42:29 2013 +0200 (2013-04-01)
changeset 51593d40aec502416
parent 51592 c3a7d6592e3f
child 51594 89bfe7a33615
added lemma
src/HOL/Lattices.thy
     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