diff -r 7d59af98af29 -r 2a4c8a2a3f8e src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 27 19:48:28 2018 +0100
@@ -591,7 +591,7 @@
     using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
   have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
     using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
-  have [simp]: "~ min (1 / 2) (min d1 d2) \<le> 0"
+  have [simp]: "\<not> min (1 / 2) (min d1 d2) \<le> 0"
     using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
   have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
        "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
@@ -670,7 +670,7 @@
   have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u
     using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>]
     by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps)
-  then have n1: "~ (pathstart g1 \<in> path_image g2)"
+  then have n1: "pathstart g1 \<notin> path_image g2"
     unfolding pathstart_def path_image_def
     using atLeastAtMost_iff by blast
   show ?rhs using \<open>?lhs\<close>
@@ -2442,7 +2442,7 @@
 lemma cobounded_unbounded_component:
     fixes s :: "'a :: euclidean_space set"
     assumes "bounded (-s)"
-      shows "\<exists>x. x \<in> s \<and> ~ bounded (connected_component_set s x)"
+      shows "\<exists>x. x \<in> s \<and> \<not> bounded (connected_component_set s x)"
 proof -
   obtain i::'a where i: "i \<in> Basis"
     using nonempty_Basis by blast
@@ -2450,7 +2450,7 @@
     using bounded_subset_ballD [OF assms, of 0] by auto
   then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
     by (force simp: ball_def dist_norm)
-  have unbounded_inner: "~ bounded {x. inner i x \<ge> B}"
+  have unbounded_inner: "\<not> bounded {x. inner i x \<ge> B}"
     apply (auto simp: bounded_def dist_norm)
     apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
     apply simp
@@ -2475,8 +2475,8 @@
 lemma cobounded_unique_unbounded_component:
     fixes s :: "'a :: euclidean_space set"
     assumes bs: "bounded (-s)" and "2 \<le> DIM('a)"
-        and bo: "~ bounded(connected_component_set s x)"
-                "~ bounded(connected_component_set s y)"
+        and bo: "\<not> bounded(connected_component_set s x)"
+                "\<not> bounded(connected_component_set s y)"
       shows "connected_component_set s x = connected_component_set s y"
 proof -
   obtain i::'a where i: "i \<in> Basis"
@@ -2507,7 +2507,7 @@
 
 lemma cobounded_unbounded_components:
     fixes s :: "'a :: euclidean_space set"
-    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> ~bounded c"
+    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> \<not>bounded c"
   by (metis cobounded_unbounded_component components_def imageI)
 
 lemma cobounded_unique_unbounded_components:
@@ -2532,9 +2532,9 @@
   "inside S \<equiv> {x. (x \<notin> S) \<and> bounded(connected_component_set ( - S) x)}"
 
 definition%important outside where
-  "outside S \<equiv> -S \<inter> {x. ~ bounded(connected_component_set (- S) x)}"
-
-lemma outside: "outside S = {x. ~ bounded(connected_component_set (- S) x)}"
+  "outside S \<equiv> -S \<inter> {x. \<not> bounded(connected_component_set (- S) x)}"
+
+lemma outside: "outside S = {x. \<not> bounded(connected_component_set (- S) x)}"
   by (auto simp: outside_def) (metis Compl_iff bounded_empty connected_component_eq_empty)
 
 lemma inside_no_overlap [simp]: "inside S \<inter> S = {}"
@@ -2619,7 +2619,7 @@
 
 lemma unbounded_outside:
     fixes S :: "'a::{real_normed_vector, perfect_space} set"
-    shows "bounded S \<Longrightarrow> ~ bounded(outside S)"
+    shows "bounded S \<Longrightarrow> \<not> bounded(outside S)"
   using cobounded_imp_unbounded cobounded_outside by blast
 
 lemma bounded_inside:
@@ -2655,7 +2655,7 @@
 lemma not_outside_connected_component_lt:
     fixes S :: "'a::euclidean_space set"
     assumes S: "bounded S" and "2 \<le> DIM('a)"
-      shows "- (outside S) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- S) x y)}"
+      shows "- (outside S) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> \<not> connected_component (- S) x y}"
 proof -
   obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
     using S [simplified bounded_pos] by auto
@@ -2681,24 +2681,24 @@
 lemma not_outside_connected_component_le:
     fixes S :: "'a::euclidean_space set"
     assumes S: "bounded S"  "2 \<le> DIM('a)"
-      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- S) x y)}"
+      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y}"
 apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
 by (meson gt_ex less_le_trans)
 
 lemma inside_connected_component_lt:
     fixes S :: "'a::euclidean_space set"
     assumes S: "bounded S"  "2 \<le> DIM('a)"
-      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- S) x y))}"
+      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> \<not> connected_component (- S) x y)}"
   by (auto simp: inside_outside not_outside_connected_component_lt [OF assms])
 
 lemma inside_connected_component_le:
     fixes S :: "'a::euclidean_space set"
     assumes S: "bounded S"  "2 \<le> DIM('a)"
-      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- S) x y))}"
+      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y)}"
   by (auto simp: inside_outside not_outside_connected_component_le [OF assms])
 
 lemma inside_subset:
-  assumes "connected U" and "~bounded U" and "T \<union> U = - S"
+  assumes "connected U" and "\<not> bounded U" and "T \<union> U = - S"
   shows "inside S \<subseteq> T"
 apply (auto simp: inside_def)
 by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
@@ -2794,7 +2794,7 @@
 lemma frontier_minimal_separating_closed:
   fixes S :: "'a::real_normed_vector set"
   assumes "closed S"
-      and nconn: "~ connected(- S)"
+      and nconn: "\<not> connected(- S)"
       and C: "C \<in> components (- S)"
       and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected(- T)"
     shows "frontier C = S"
@@ -3319,7 +3319,7 @@
 
 lemma bounded_unique_outside:
     fixes s :: "'a :: euclidean_space set"
-    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> ~bounded c \<longleftrightarrow> c = outside s)"
+    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> \<not> bounded c \<longleftrightarrow> c = outside s)"
   apply (rule iffI)
   apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
   by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
@@ -3365,7 +3365,7 @@
       apply (rule le_no)
       using w wy oint
       by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
-    have **: "(~(b \<inter> (- S) = {}) \<and> ~(b - (- S) = {}) \<Longrightarrow> (b \<inter> f \<noteq> {}))
+    have **: "(b \<inter> (- S) \<noteq> {} \<and> b - (- S) \<noteq> {} \<Longrightarrow> b \<inter> f \<noteq> {})
               \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
               b \<subseteq> S" for b f and S :: "'b set"
       by blast
@@ -5065,7 +5065,7 @@
     done
 qed
 
-subsection\<open>Sort of induction principle for connected sets\<close>
+subsection\<open>An induction principle for connected sets\<close>
 
 proposition connected_induction:
   assumes "connected S"
@@ -5084,7 +5084,7 @@
     done
   have 2: "openin (subtopology euclidean S)
              {b. \<exists>T. openin (subtopology euclidean S) T \<and>
-                     b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> ~ Q x)}"
+                     b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
     apply (subst openin_subopen, clarify)
     apply (rule_tac x=T in exI, auto)
     done
@@ -5742,7 +5742,7 @@
 qed blast
 
 
-subsection\<open>Important special cases of local connectedness and path connectedness\<close>
+subsection\<open>Special cases of local connectedness and path connectedness\<close>
 
 lemma locally_connected_1:
   assumes
@@ -7155,7 +7155,7 @@
 
 lemma connected_card_eq_iff_nontrivial:
   fixes S :: "'a::metric_space set"
-  shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> ~(\<exists>a. S \<subseteq> {a})"
+  shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> \<not>(\<exists>a. S \<subseteq> {a})"
   apply (auto simp: countable_finite finite_subset)
   by (metis connected_uncountable is_singletonI' is_singleton_the_elem subset_singleton_iff)
 
@@ -7184,7 +7184,7 @@
 
 proposition path_connected_convex_diff_countable:
   fixes U :: "'a::euclidean_space set"
-  assumes "convex U" "~ collinear U" "countable S"
+  assumes "convex U" "\<not> collinear U" "countable S"
     shows "path_connected(U - S)"
 proof (clarsimp simp add: path_connected_def)
   fix a b
@@ -7202,7 +7202,7 @@
     have "?m \<in> U"
       using \<open>a \<in> U\<close> \<open>b \<in> U\<close> \<open>convex U\<close> convex_contains_segment by force
     obtain c where "c \<in> U" and nc_abc: "\<not> collinear {a,b,c}"
-      by (metis False \<open>a \<in> U\<close> \<open>b \<in> U\<close> \<open>~ collinear U\<close> collinear_triples insert_absorb)
+      by (metis False \<open>a \<in> U\<close> \<open>b \<in> U\<close> \<open>\<not> collinear U\<close> collinear_triples insert_absorb)
     have ncoll_mca: "\<not> collinear {?m,c,a}"
       by (metis (full_types) \<open>a \<noteq> ?m\<close> collinear_3_trans collinear_midpoint insert_commute nc_abc)
     have ncoll_mcb: "\<not> collinear {?m,c,b}"
@@ -7289,7 +7289,7 @@
 
 corollary connected_convex_diff_countable:
   fixes U :: "'a::euclidean_space set"
-  assumes "convex U" "~ collinear U" "countable S"
+  assumes "convex U" "\<not> collinear U" "countable S"
   shows "connected(U - S)"
   by (simp add: assms path_connected_convex_diff_countable path_connected_imp_connected)
 
@@ -7344,7 +7344,7 @@
 proposition path_connected_openin_diff_countable:
   fixes S :: "'a::euclidean_space set"
   assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S"
-      and "~ collinear S" "countable T"
+      and "\<not> collinear S" "countable T"
     shows "path_connected(S - T)"
 proof (clarsimp simp add: path_connected_component)
   fix x y
@@ -7360,8 +7360,8 @@
         by (auto simp: openin_contains_ball)
       with \<open>x \<in> U\<close> have x: "x \<in> ball x r \<inter> affine hull S"
         by auto
-      have "~ S \<subseteq> {x}"
-        using \<open>~ collinear S\<close>  collinear_subset by blast
+      have "\<not> S \<subseteq> {x}"
+        using \<open>\<not> collinear S\<close>  collinear_subset by blast
       then obtain x' where "x' \<noteq> x" "x' \<in> S"
         by blast
       obtain y where y: "y \<noteq> x" "y \<in> ball x r \<inter> affine hull S"
@@ -7414,7 +7414,7 @@
 corollary connected_openin_diff_countable:
   fixes S :: "'a::euclidean_space set"
   assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S"
-      and "~ collinear S" "countable T"
+      and "\<not> collinear S" "countable T"
     shows "connected(S - T)"
   by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms])
 
@@ -7445,7 +7445,7 @@
 
 
 
-subsection\<open>Self-homeomorphisms shuffling points about in various ways\<close>
+subsection\<open>Self-homeomorphisms shuffling points about\<close>
 
 subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
 
@@ -7610,7 +7610,7 @@
   assumes "affine T" "a \<in> T" and ST: "ball a r \<inter> T \<subseteq> S" "S \<subseteq> T"
       and u: "u \<in> ball a r \<inter> T" and v: "v \<in> ball a r \<inter> T"
   obtains f g where "homeomorphism S S f g"
-                    "f u = v" "{x. ~ (f x = x \<and> g x = x)} \<subseteq> ball a r \<inter> T"
+                    "f u = v" "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> ball a r \<inter> T"
 proof -
   obtain f g where hom: "homeomorphism (cball a r \<inter> T) (cball a r \<inter> T) f g"
                and "f u = v" and fid: "\<And>x. \<lbrakk>x \<in> sphere a r; x \<in> T\<rbrakk> \<Longrightarrow> f x = x"
@@ -7690,14 +7690,14 @@
       and TS: "T \<subseteq> affine hull S"
       and S: "connected S" "a \<in> S" "b \<in> S"
   obtains f g where "homeomorphism T T f g" "f a = b"
-                    "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S"
-                    "bounded {x. ~ (f x = x \<and> g x = x)}"
+                    "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S"
+                    "bounded {x. \<not> (f x = x \<and> g x = x)}"
 proof -
   have 1: "\<exists>h k. homeomorphism T T h k \<and> h (f d) = d \<and>
-              {x. ~ (h x = x \<and> k x = x)} \<subseteq> S \<and> bounded {x. ~ (h x = x \<and> k x = x)}"
+              {x. \<not> (h x = x \<and> k x = x)} \<subseteq> S \<and> bounded {x. \<not> (h x = x \<and> k x = x)}"
         if "d \<in> S" "f d \<in> S" and homfg: "homeomorphism T T f g"
-        and S: "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S"
-        and bo: "bounded {x. ~ (f x = x \<and> g x = x)}" for d f g
+        and S: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S"
+        and bo: "bounded {x. \<not> (f x = x \<and> g x = x)}" for d f g
   proof (intro exI conjI)
     show homgf: "homeomorphism T T g f"
       by (metis homeomorphism_symD homfg)
@@ -7722,7 +7722,7 @@
       by force
     show "{x. \<not> ((f2 \<circ> f1) x = x \<and> (g1 \<circ> g2) x = x)} \<subseteq> S"
       using sub by force
-    have "bounded ({x. ~(f1 x = x \<and> g1 x = x)} \<union> {x. ~(f2 x = x \<and> g2 x = x)})"
+    have "bounded ({x. \<not>(f1 x = x \<and> g1 x = x)} \<union> {x. \<not>(f2 x = x \<and> g2 x = x)})"
       using bo by simp
     then show "bounded {x. \<not> ((f2 \<circ> f1) x = x \<and> (g1 \<circ> g2) x = x)}"
       by (rule bounded_subset) auto
@@ -7753,7 +7753,7 @@
       done
   qed
   have "\<exists>f g. homeomorphism T T f g \<and> f a = b \<and>
-              {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
+              {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
     apply (rule connected_equivalence_relation [OF S], safe)
       apply (blast intro: 1 2 3)+
     done
@@ -7769,7 +7769,7 @@
       and ope: "openin (subtopology euclidean (affine hull S)) S"
       and "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   shows "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(x i) = y i) \<and>
-               {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
+               {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
   using assms
 proof (induction K)
   case empty
@@ -7783,11 +7783,11 @@
        and xyS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
     by (simp_all add: pairwise_insert)
   obtain f g where homfg: "homeomorphism T T f g" and feq: "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
-               and fg_sub: "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S"
-               and bo_fg: "bounded {x. ~ (f x = x \<and> g x = x)}"
+               and fg_sub: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S"
+               and bo_fg: "bounded {x. \<not> (f x = x \<and> g x = x)}"
     using insert.IH [OF xyS pw] insert.prems by (blast intro: that)
   then have "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(x i) = y i) \<and>
-                   {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
+                   {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
     using insert by blast
   have aff_eq: "affine hull (S - y ` K) = affine hull S"
     apply (rule affine_hull_Diff)
@@ -7832,7 +7832,7 @@
       using feq hk_sub by (auto simp: heq)
     show "{x. \<not> ((h \<circ> f) x = x \<and> (g \<circ> k) x = x)} \<subseteq> S"
       using fg_sub hk_sub by force
-    have "bounded ({x. ~(f x = x \<and> g x = x)} \<union> {x. ~(h x = x \<and> k x = x)})"
+    have "bounded ({x. \<not>(f x = x \<and> g x = x)} \<union> {x. \<not>(h x = x \<and> k x = x)})"
       using bo_fg bo_hk bounded_Un by blast
     then show "bounded {x. \<not> ((h \<circ> f) x = x \<and> (g \<circ> k) x = x)}"
       by (rule bounded_subset) auto
@@ -7846,7 +7846,7 @@
       and pw: "pairwise (\<lambda>i j. (x i \<noteq> x j) \<and> (y i \<noteq> y j)) K"
       and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
-                    "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
+                    "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (\<not> (f x = x \<and> g x = x))}"
 proof (cases "S = {}")
   case True
   then show ?thesis
@@ -7995,8 +7995,8 @@
   fixes T :: "real set"
   assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
   obtains f g where "homeomorphism T T f g"
-                    "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
-                    "bounded {x. (~ (f x = x \<and> g x = x))}"
+                    "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
+                    "bounded {x. (\<not> (f x = x \<and> g x = x))}"
 proof -
   obtain c d where "box c d \<noteq> {}" "cbox c d \<subseteq> U"
   proof -
@@ -8109,8 +8109,8 @@
 proposition homeomorphism_grouping_points_exists:
   fixes S :: "'a::euclidean_space set"
   assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
-  obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
-                    "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
+  obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
+                    "bounded {x. (\<not> (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
 proof (cases "2 \<le> DIM('a)")
   case True
   have TS: "T \<subseteq> affine hull S"
@@ -8172,10 +8172,10 @@
       using sub hj
       apply (drule_tac c="h x" in subsetD, force)
       by (metis imageE)
-    have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
+    have "bounded (j ` {x. (\<not> (f x = x \<and> g x = x))})"
       by (rule bounded_linear_image [OF bou]) (use \<open>linear j\<close> linear_conv_bounded_linear in auto)
     moreover
-    have *: "{x. ~((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)} = j ` {x. (~ (f x = x \<and> g x = x))}"
+    have *: "{x. \<not>((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)} = j ` {x. (\<not> (f x = x \<and> g x = x))}"
       using hj by (auto simp: jf jg image_iff, metis+)
     ultimately show "bounded {x. \<not> ((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)}"
       by metis
@@ -8190,8 +8190,8 @@
   assumes opeU: "openin (subtopology euclidean S) U"
       and opeS: "openin (subtopology euclidean (affine hull S)) S"
       and "U \<noteq> {}" "finite K" "K \<subseteq> S" and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
-  obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
-                    "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
+  obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
+                    "bounded {x. (\<not> (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
 proof (cases "2 \<le> aff_dim S")
   case True
   have opeU': "openin (subtopology euclidean (affine hull S)) U"
@@ -8208,7 +8208,7 @@
   then obtain \<gamma> where \<gamma>: "bij_betw \<gamma> K P"
     using \<open>finite K\<close> finite_same_card_bij by blast
   have "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(id i) = \<gamma> i) \<and>
-               {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
+               {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
   proof (rule homeomorphism_moving_points_exists_gen [OF \<open>finite K\<close> _ _ True opeS S])
     show "\<And>i. i \<in> K \<Longrightarrow> id i \<in> S \<and> \<gamma> i \<in> S"
       by (metis id_apply opeU openin_contains_cball subsetCE \<open>P \<subseteq> U\<close> \<open>bij_betw \<gamma> K P\<close> \<open>K \<subseteq> S\<close> bij_betwE)
@@ -8314,10 +8314,10 @@
     next
       have "compact (j ` closure {x. \<not> (f x = x \<and> g x = x)})"
         using bou by (auto simp: compact_continuous_image cont_hj)
-      then have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
+      then have "bounded (j ` {x. \<not> (f x = x \<and> g x = x)})"
         by (rule bounded_closure_image [OF compact_imp_bounded])
       moreover
-      have *: "{x \<in> affine hull S. j (f (h x)) \<noteq> x \<or> j (g (h x)) \<noteq> x} = j ` {x. (~ (f x = x \<and> g x = x))}"
+      have *: "{x \<in> affine hull S. j (f (h x)) \<noteq> x \<or> j (g (h x)) \<noteq> x} = j ` {x. (\<not> (f x = x \<and> g x = x))}"
         using h j by (auto simp: image_iff; metis)
       ultimately have "bounded {x \<in> affine hull S. j (f (h x)) \<noteq> x \<or> j (g (h x)) \<noteq> x}"
         by metis
@@ -8337,7 +8337,7 @@
   qed
 qed
 
-subsection\<open>nullhomotopic mappings\<close>
+subsection\<open>Nullhomotopic mappings\<close>
 
 text\<open> A mapping out of a sphere is nullhomotopic iff it extends to the ball.
 This even works out in the degenerate cases when the radius is \<open>\<le>\<close> 0, and