src/HOL/Library/Convex.thy
changeset 61585 a9599d3d7610
parent 61531 ab2e862263e7
child 61694 6571c78c9667
     1.1 --- a/src/HOL/Library/Convex.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/Convex.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -883,7 +883,7 @@
     1.4    fix t x y :: real
     1.5    assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
     1.6    def z \<equiv> "(1 - t) * x + t * y"
     1.7 -  with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
     1.8 +  with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
     1.9    
    1.10    from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
    1.11    have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)