src/HOL/Lattices.thy
changeset 27682 25aceefd4786
parent 26794 354c3844dfde
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Lattices.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -32,8 +32,8 @@
     1.4  
     1.5  lemma dual_lattice:
     1.6    "lower_semilattice (op \<ge>) (op >) sup"
     1.7 -by unfold_locales
     1.8 -  (auto simp add: sup_least)
     1.9 +by (rule lower_semilattice.intro, rule dual_order)
    1.10 +  (unfold_locales, simp_all add: sup_least)
    1.11  
    1.12  end
    1.13