src/HOL/Lattices.thy

--- a/src/HOL/Lattices.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Lattices.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -32,8 +32,8 @@
 
 lemma dual_lattice:
   "lower_semilattice (op \<ge>) (op >) sup"
-by unfold_locales
-  (auto simp add: sup_least)
+by (rule lower_semilattice.intro, rule dual_order)
+  (unfold_locales, simp_all add: sup_least)
 
 end