--- a/src/HOL/Lattices.thy Fri Jan 16 08:29:11 2009 +0100
+++ b/src/HOL/Lattices.thy Fri Jan 16 14:58:11 2009 +0100
@@ -300,8 +300,7 @@
by auto
qed (auto simp add: min_def max_def not_le less_imp_le)
-class_interpretation min_max:
- distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
+interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
by (rule distrib_lattice_min_max)
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"