author | nipkow |
Mon, 01 Apr 2013 17:42:29 +0200 | |
changeset 51593 | d40aec502416 |
parent 51592 | c3a7d6592e3f |
child 51594 | 89bfe7a33615 |
--- 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