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