src/HOL/Analysis/Convex_Euclidean_Space.thy

--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
@@ -1343,7 +1343,9 @@
   by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
 
 
-subsubsection%unimportant \<open>Some explicit formulations (from Lars Schewe)\<close>
+subsubsection%unimportant \<open>Some explicit formulations\<close>
+
+text "Formalized by Lars Schewe."
 
 lemma affine:
   fixes V::"'a::real_vector set"
@@ -2070,7 +2072,9 @@
 qed
 
 
-subsection \<open>Affine dependence and consequential theorems (from Lars Schewe)\<close>
+subsection \<open>Affine dependence and consequential theorems\<close>
+
+text "Formalized by Lars Schewe."
 
 definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
@@ -2082,11 +2086,11 @@
 done
 
 lemma affine_independent_subset:
-  shows "\<lbrakk>~ affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> ~ affine_dependent s"
+  shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
 by (metis affine_dependent_subset)
 
 lemma affine_independent_Diff:
-   "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
+   "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
 by (meson Diff_subset affine_dependent_subset)
 
 proposition affine_dependent_explicit:
@@ -2601,7 +2605,9 @@
 qed (use assms in \<open>auto simp: convex_explicit\<close>)
 
 
-subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
+subsubsection%unimportant \<open>Another formulation\<close>
+
+text "Formalized by Lars Schewe."
 
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
@@ -3427,7 +3433,7 @@
 
 lemma affine_independent_iff_card:
     fixes s :: "'a::euclidean_space set"
-    shows "~ affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
+    shows "\<not> affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
   apply (rule iffI)
   apply (simp add: aff_dim_affine_independent aff_independent_finite)
   by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
@@ -3652,7 +3658,7 @@
 
 lemma affine_independent_card_dim_diffs:
   fixes S :: "'a :: euclidean_space set"
-  assumes "~ affine_dependent S" "a \<in> S"
+  assumes "\<not> affine_dependent S" "a \<in> S"
     shows "card S = dim {x - a|x. x \<in> S} + 1"
 proof -
   have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
@@ -3766,7 +3772,7 @@
   show ?thesis
   proof safe
     assume 0: "aff_dim S = 0"
-    have "~ {a,b} \<subseteq> S" if "b \<noteq> a" for b
+    have "\<not> {a,b} \<subseteq> S" if "b \<noteq> a" for b
       by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
     then show "\<exists>a. S = {a}"
       using \<open>a \<in> S\<close> by blast
@@ -3798,7 +3804,7 @@
 
 lemma disjoint_affine_hull:
   fixes s :: "'n::euclidean_space set"
-  assumes "~ affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
+  assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
     shows "(affine hull t) \<inter> (affine hull u) = {}"
 proof -
   have "finite s" using assms by (simp add: aff_independent_finite)
@@ -3813,7 +3819,7 @@
     have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
     have "sum c s = 0"
       by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
-    moreover have "~ (\<forall>v\<in>s. c v = 0)"
+    moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
       by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum_not_0 zero_neq_one)
     moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
       by (simp add: c_def if_smult sum_negf
@@ -5747,7 +5753,9 @@
 qed auto
 
 
-subsection \<open>Radon's theorem (from Lars Schewe)\<close>
+subsection \<open>Radon's theorem\<close>
+
+text "Formalized by Lars Schewe."
 
 lemma radon_ex_lemma:
   assumes "finite c" "affine_dependent c"