src/HOL/Lattices.thy
changeset 29223 e09c53289830
parent 28823 dcbef866c9e2
child 29509 1ff0f3f08a7b
     1.1 --- a/src/HOL/Lattices.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -300,7 +300,7 @@
     1.4    by auto
     1.5  qed (auto simp add: min_def max_def not_le less_imp_le)
     1.6  
     1.7 -interpretation min_max:
     1.8 +class_interpretation min_max:
     1.9    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
    1.10    by (rule distrib_lattice_min_max)
    1.11