src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 67155 9e5b05d54f9d
parent 67135 1a94352812f4
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Dec 05 12:14:36 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 07 15:48:50 2017 +0100
     1.3 @@ -7262,7 +7262,7 @@
     1.4        unfolding 2
     1.5        apply clarsimp
     1.6        apply (subst euclidean_dist_l2)
     1.7 -      apply (rule order_trans [OF setL2_le_sum])
     1.8 +      apply (rule order_trans [OF L2_set_le_sum])
     1.9        apply (rule zero_le_dist)
    1.10        unfolding e'
    1.11        apply (rule sum_mono)