src/HOL/Finite_Set.thy

   "lower_semilattice (op \<ge>) (op >) max"
   by (fact min_max.dual_semilattice)
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw expand_fun_eq)
+  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw expand_fun_eq)
+  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"
   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -