src/HOL/Complete_Lattice.thy
changeset 36635 080b755377c0
parent 36364 0e2679025aeb
child 37767 a2b7a20d6ea3
     1.1 --- a/src/HOL/Complete_Lattice.thy	Tue May 04 08:55:39 2010 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Tue May 04 08:55:43 2010 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4  begin
     1.5  
     1.6  lemma dual_complete_lattice:
     1.7 -  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
     1.8 -  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
     1.9 +  "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.10 +  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
    1.11      (unfold_locales, (fact bot_least top_greatest
    1.12          Sup_upper Sup_least Inf_lower Inf_greatest)+)
    1.13