--- a/src/HOL/Complete_Lattices.thy Tue Mar 26 15:10:28 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Mar 26 20:49:57 2013 +0100
@@ -514,10 +514,10 @@
by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
lemma complete_linorder_inf_min: "inf = min"
- by (rule ext)+ (auto intro: antisym simp add: min_def)
+ by (auto intro: antisym simp add: min_def fun_eq_iff)
lemma complete_linorder_sup_max: "sup = max"
- by (rule ext)+ (auto intro: antisym simp add: max_def)
+ by (auto intro: antisym simp add: max_def fun_eq_iff)
lemma Inf_less_iff:
"\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"