changeset 67155 | 9e5b05d54f9d |
parent 67135 | 1a94352812f4 |
child 67399 | eab6ce8368fa |
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 07 11:14:32 2017 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Dec 07 15:48:50 2017 +0100 @@ -7262,7 +7262,7 @@ unfolding 2 apply clarsimp apply (subst euclidean_dist_l2) - apply (rule order_trans [OF setL2_le_sum]) + apply (rule order_trans [OF L2_set_le_sum]) apply (rule zero_le_dist) unfolding e' apply (rule sum_mono)