summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)