src/HOL/Lattices.thy
changeset 23087 ad7244663431
parent 23018 1d29bc31b0cb
child 23389 aaca6a8e5414
     1.1 --- a/src/HOL/Lattices.thy	Thu May 24 08:37:37 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Thu May 24 08:37:39 2007 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  
     1.5  interpretation min_max:
     1.6    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
     1.7 -  by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max])
     1.8 +  by (rule distrib_lattice_min_max [folded ord_class.min ord_class.max])
     1.9  
    1.10  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.11    by (rule ext)+ auto