changeset 54863 | 82acc20ded73 |
parent 54797 | be020ec8560c |
child 55415 | 05f5fdb8d093 |
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Dec 25 17:39:06 2013 +0100 @@ -2527,7 +2527,7 @@ apply (drule (1) bspec) apply simp apply (drule (1) bspec) - apply (rule min_max.le_supI2) + apply (rule max.coboundedI2) apply (erule order_trans [OF dist_triangle add_left_mono]) done