src/HOL/Finite_Set.thy

   \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> h (Max N) = Max (h ` N)"
   by (simp add: Max_def ACIf.hom_fold1_commute [OF ACIf_max])
 
 end
 
-class linordered_ab_semigroup_add = linorder + pordered_ab_semigroup_add
+context ordered_ab_semigroup_add
 begin
 
 lemma add_Min_commute:
   fixes k
   shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k \<^loc>+ Min N = Min {k \<^loc>+ m | m. m \<in> N}"