--- a/src/HOL/Finite_Set.thy Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/Finite_Set.thy Fri Aug 28 19:15:59 2009 +0200
@@ -2966,11 +2966,11 @@
lemma dual_max:
"ord.max (op \<ge>) = min"
- by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
+ by (auto simp add: ord.max_def_raw expand_fun_eq)
lemma dual_min:
"ord.min (op \<ge>) = max"
- by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
+ by (auto simp add: ord.min_def_raw expand_fun_eq)
lemma strict_below_fold1_iff:
assumes "finite A" and "A \<noteq> {}"