src/HOL/Multivariate_Analysis/Polytope.thy

       using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by simp
     show ?thesis
       apply (rule zne [OF in01])
       apply (rule e [THEN subsetD])
       apply (rule IntI)
-        using `y \<noteq> x` \<open>e > 0\<close>
+        using \<open>y \<noteq> x\<close> \<open>e > 0\<close>
         apply (simp add: cball_def dist_norm algebra_simps)
         apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
       apply (rule mem_affine [OF affine_affine_hull _ x])
       using \<open>y \<in> T\<close>  apply (auto simp: hull_inc)
       done

       using False nbc \<open>0 < e\<close>
       apply (auto simp: algebra_simps)
       done
     then have "d \<in> T \<and> c \<in> T"
       apply (rule face_ofD [OF \<open>T face_of S\<close>])
-      using `d \<in> u`  `c \<in> u` \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
+      using \<open>d \<in> u\<close>  \<open>c \<in> u\<close> \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
       done
     then show ?thesis ..
   qed
 qed
 

         then have "setsum c T = 0"
           by (simp add: S k_def setsum_diff sumc1)
         then have [simp]: "setsum c (S - T) = 1"
           by (simp add: S setsum_diff sumc1)
         have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
-          by (meson `finite T` `setsum c T = 0` \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
+          by (meson \<open>finite T\<close> \<open>setsum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
         then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
           by (simp add: weq_sumsum)
         have "w \<in> convex hull (S - T)"
           apply (simp add: convex_hull_finite fin)
           apply (rule_tac x=c in exI)

           apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
           apply auto
           apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE)
           apply (metis False mult.commute right_inverse right_minus_eq setsum_right_distrib sumcf)
           by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong)
-        with `0 < k`  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
+        with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
           by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
         moreover have "inverse(k) *\<^sub>R (w - setsum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
           apply (simp add: weq_sumsum convex_hull_finite fin)
           apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
           using \<open>k > 0\<close> cge0

       ultimately show ?thesis
         by (rule face_ofD [OF \<open>T face_of S\<close>, THEN conjunct2])
     qed
   qed
   then show False
-    using `T \<noteq> S` \<open>T face_of S\<close> face_of_imp_subset by blast
+    using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
 qed
 
 
 lemma face_of_affine_eq:
    "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"

 proof -
   have "finite S" by (metis assms aff_independent_finite)
   then consider "card S = 0" | "card S = 1" | "2 \<le> card S" by arith
   then show ?thesis
   proof cases
-    case 1 then have "S = {}" by (simp add: `finite S`)
+    case 1 then have "S = {}" by (simp add: \<open>finite S\<close>)
     then show ?thesis by simp
   next
     case 2 show ?thesis
-      by (auto intro: card_1_singletonE [OF `card S = 1`])
+      by (auto intro: card_1_singletonE [OF \<open>card S = 1\<close>])
   next
     case 3
     with assms show ?thesis
       by (auto simp: polyhedron_convex_hull rel_boundary_of_polyhedron facet_of_convex_hull_affine_independent_alt \<open>finite S\<close>)
   qed

       then obtain a where "a \<in> S" "a \<notin> T"
         using \<open>T \<subseteq> S\<close> by blast
       then have "x \<in> (\<Union>a\<in>S. convex hull (S - {a}))"
         using True affine_independent_iff_card [of S]
         apply simp
-        apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 `a \<notin> T` `T \<subseteq> S` `x \<in> convex hull T`  hull_mono insert_Diff_single   subsetCE)
+        apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 \<open>a \<notin> T\<close> \<open>T \<subseteq> S\<close> \<open>x \<in> convex hull T\<close>  hull_mono insert_Diff_single   subsetCE)
         done
     } note * = this
     have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
       apply (subst caratheodory_aff_dim)
       apply (blast intro: *)