--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 07 16:48:10 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 07 20:19:59 2015 +0100
@@ -266,7 +266,7 @@
have [simp]: "g ` f ` S = S"
using g by (simp add: image_comp)
have cgf: "closed (g ` f ` S)"
- by (simp add: `g \<circ> f = id` S image_comp)
+ by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
have [simp]: "{x \<in> range f. g x \<in> S} = f ` S"
using g by (simp add: o_def id_def image_def) metis
show ?thesis
@@ -5695,7 +5695,7 @@
apply auto
done
-subsection \<open>On @{text "real"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent.\<close>
+subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
lemma is_interval_1:
"is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
@@ -9132,7 +9132,7 @@
{ fix u v x
assume uv: "setsum u t = 1" "\<forall>x\<in>s. 0 \<le> v x" "setsum v s = 1"
"(\<Sum>x\<in>s. v x *\<^sub>R x) = (\<Sum>v\<in>t. u v *\<^sub>R v)" "x \<in> t"
- then have s: "s = (s - t) \<union> t" --\<open>split into separate cases\<close>
+ then have s: "s = (s - t) \<union> t" \<comment>\<open>split into separate cases\<close>
using assms by auto
have [simp]: "(\<Sum>x\<in>t. v x *\<^sub>R x) + (\<Sum>x\<in>s - t. v x *\<^sub>R x) = (\<Sum>x\<in>t. u x *\<^sub>R x)"
"setsum v t + setsum v (s - t) = 1"
@@ -9250,7 +9250,7 @@
using assms by (simp add: aff_independent_finite)
{ fix a b and d::real
assume ab: "a \<in> s" "b \<in> s" "a \<noteq> b"
- then have s: "s = (s - {a,b}) \<union> {a,b}" --\<open>split into separate cases\<close>
+ then have s: "s = (s - {a,b}) \<union> {a,b}" \<comment>\<open>split into separate cases\<close>
by auto
have "(\<Sum>x\<in>s. if x = a then - d else if x = b then d else 0) = 0"
"(\<Sum>x\<in>s. (if x = a then - d else if x = b then d else 0) *\<^sub>R x) = d *\<^sub>R b - d *\<^sub>R a"