changeset 36092 | 8f1e60d9f7cc |
parent 34209 | c7f621786035 |
child 36096 | abc6a2ea4b88 |
--- a/src/HOL/Lattices.thy Thu Feb 11 21:00:36 2010 +0100 +++ b/src/HOL/Lattices.thy Mon Feb 15 01:27:06 2010 +0100 @@ -301,8 +301,7 @@ lemma dual_bounded_lattice: "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" - by (rule bounded_lattice.intro, rule dual_lattice) - (unfold_locales, auto simp add: less_le_not_le) + by unfold_locales (auto simp add: less_le_not_le) lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>"