changeset 54863 | 82acc20ded73 |
parent 54489 | 03ff4d1e6784 |
child 55945 | e96383acecf9 |
--- a/src/HOL/Real.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/Real.thy Wed Dec 25 17:39:06 2013 +0100 @@ -632,7 +632,7 @@ "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max" instance proof -qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1) +qed (auto simp add: inf_real_def sup_real_def max_min_distrib2) end