tuned headers; ~ -> \<not>
authornipkow
Thu Dec 27 19:48:28 2018 +0100 (4 months ago)
changeset 695082a4c8a2a3f8e
parent 69506 7d59af98af29
child 69509 f9bf65d90b69
tuned headers; ~ -> \<not>
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Cross3.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Improper_Integral.thy
src/HOL/Analysis/Jordan_Curve.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Poly_Roots.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Riemann_Mapping.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Analysis/Winding_Numbers.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Dec 26 20:57:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Dec 27 19:48:28 2018 +0100
     1.3 @@ -1979,7 +1979,7 @@
     1.4  
     1.5  definition connected_space :: "'a topology \<Rightarrow> bool" where
     1.6    "connected_space X \<equiv>
     1.7 -        ~(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
     1.8 +        \<not>(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
     1.9                    topspace X \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
    1.10  
    1.11  definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.12 @@ -2093,10 +2093,10 @@
    1.13  lemma connectedin_closedin:
    1.14     "connectedin X S \<longleftrightarrow>
    1.15          S \<subseteq> topspace X \<and>
    1.16 -        ~(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
    1.17 +        \<not>(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
    1.18                    S \<subseteq> (E1 \<union> E2) \<and>
    1.19                    (E1 \<inter> E2 \<inter> S = {}) \<and>
    1.20 -                  ~(E1 \<inter> S = {}) \<and> ~(E2 \<inter> S = {}))"
    1.21 +                  \<not>(E1 \<inter> S = {}) \<and> \<not>(E2 \<inter> S = {}))"
    1.22  proof -
    1.23    have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
    1.24               R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
    1.25 @@ -2269,7 +2269,7 @@
    1.26    unfolding connectedin_eq_not_separated_subset  by blast
    1.27  
    1.28  lemma connectedin_nonseparated_union:
    1.29 -   "\<lbrakk>connectedin X S; connectedin X T; ~separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
    1.30 +   "\<lbrakk>connectedin X S; connectedin X T; \<not>separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
    1.31    apply (simp add: connectedin_eq_not_separated_subset, auto)
    1.32      apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
    1.33    apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
     2.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Dec 26 20:57:23 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Dec 27 19:48:28 2018 +0100
     2.3 @@ -1060,7 +1060,7 @@
     2.4  
     2.5  text \<open>More properties of ARs, ANRs and ENRs\<close>
     2.6  
     2.7 -lemma not_AR_empty [simp]: "~ AR({})"
     2.8 +lemma not_AR_empty [simp]: "\<not> AR({})"
     2.9    by (auto simp: AR_def)
    2.10  
    2.11  lemma ENR_empty [simp]: "ENR {}"
    2.12 @@ -3823,7 +3823,7 @@
    2.13  lemma non_extensible_Borsuk_map:
    2.14    fixes a :: "'a :: euclidean_space"
    2.15    assumes "compact s" and cin: "c \<in> components(- s)" and boc: "bounded c" and "a \<in> c"
    2.16 -    shows "~ (\<exists>g. continuous_on (s \<union> c) g \<and>
    2.17 +    shows "\<not> (\<exists>g. continuous_on (s \<union> c) g \<and>
    2.18                    g ` (s \<union> c) \<subseteq> sphere 0 1 \<and>
    2.19                    (\<forall>x \<in> s. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
    2.20  proof -
    2.21 @@ -4534,7 +4534,7 @@
    2.22    fixes a :: "'a :: euclidean_space"
    2.23    assumes "compact S" and "a \<notin> S"
    2.24     shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
    2.25 -          ~(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
    2.26 +          \<not>(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
    2.27                                 (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"
    2.28     (is "?lhs = ?rhs")
    2.29  proof (cases "S = {}")
    2.30 @@ -4550,9 +4550,9 @@
    2.31      by (simp add: \<open>a \<notin> S\<close>)
    2.32    obtain r where "r>0" and r: "S \<subseteq> ball 0 r"
    2.33      using bounded_subset_ballD \<open>bounded S\<close> by blast
    2.34 -  have "~ ?rhs \<longleftrightarrow> ~ ?lhs"
    2.35 +  have "\<not> ?rhs \<longleftrightarrow> \<not> ?lhs"
    2.36    proof
    2.37 -    assume notr: "~ ?rhs"
    2.38 +    assume notr: "\<not> ?rhs"
    2.39      have nog: "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
    2.40                     g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
    2.41                     (\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a))"
    2.42 @@ -4564,12 +4564,12 @@
    2.43        using notr
    2.44        by (auto simp: nullhomotopic_into_sphere_extension
    2.45                   [OF \<open>closed S\<close> continuous_on_Borsuk_map [OF \<open>a \<notin> S\<close>] False s01])
    2.46 -    with \<open>a \<notin> S\<close> show  "~ ?lhs"
    2.47 +    with \<open>a \<notin> S\<close> show  "\<not> ?lhs"
    2.48        apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog)
    2.49        apply (drule_tac x=g in spec)
    2.50        using continuous_on_subset by fastforce 
    2.51    next
    2.52 -    assume "~ ?lhs"
    2.53 +    assume "\<not> ?lhs"
    2.54      then obtain b where b: "b \<in> connected_component_set (- S) a" and "r \<le> norm b"
    2.55        using bounded_iff linear by blast
    2.56      then have bnot: "b \<notin> ball 0 r"
    2.57 @@ -4593,7 +4593,7 @@
    2.58      ultimately have "homotopic_with (\<lambda>x. True) S (sphere 0 1)
    2.59                           (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
    2.60        by (meson homotopic_with_subset_left homotopic_with_trans r)
    2.61 -    then show "~ ?rhs"
    2.62 +    then show "\<not> ?rhs"
    2.63        by blast
    2.64    qed
    2.65    then show ?thesis by blast
     3.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
     3.3 @@ -651,7 +651,7 @@
     3.4  
     3.5  lemma%unimportant Lim_component_eq_cart:
     3.6    fixes f :: "'a \<Rightarrow> real^'n"
     3.7 -  assumes net: "(f \<longlongrightarrow> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
     3.8 +  assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
     3.9    shows "l$i = b"
    3.10    using ev[unfolded order_eq_iff eventually_conj_iff] and
    3.11      Lim_component_ge_cart[OF net, of b i] and
    3.12 @@ -1060,7 +1060,7 @@
    3.13  
    3.14  lemma%unimportant matrix_nonfull_linear_equations_eq:
    3.15    fixes A :: "real^'n^'m"
    3.16 -  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> ~(rank A = CARD('n))"
    3.17 +  shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)"
    3.18    by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
    3.19  
    3.20  lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0"
     4.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Dec 26 20:57:23 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Dec 27 19:48:28 2018 +0100
     4.3 @@ -941,7 +941,7 @@
     4.4    case True then show ?thesis
     4.5      by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath)
     4.6  next
     4.7 -  case False then have "~ f contour_integrable_on (reversepath g)"
     4.8 +  case False then have "\<not> f contour_integrable_on (reversepath g)"
     4.9      by (simp add: assms contour_integrable_reversepath_eq)
    4.10    with False show ?thesis by (simp add: not_integrable_contour_integral)
    4.11  qed
    4.12 @@ -5518,7 +5518,7 @@
    4.13        and ul_f: "uniform_limit (path_image \<gamma>) f l F"
    4.14        and noleB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
    4.15        and \<gamma>: "valid_path \<gamma>"
    4.16 -      and [simp]: "~ (trivial_limit F)"
    4.17 +      and [simp]: "\<not> trivial_limit F"
    4.18    shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
    4.19  proof -
    4.20    have "0 \<le> B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
    4.21 @@ -5586,7 +5586,7 @@
    4.22  corollary%unimportant contour_integral_uniform_limit_circlepath:
    4.23    assumes "\<forall>\<^sub>F n::'a in F. (f n) contour_integrable_on (circlepath z r)"
    4.24        and "uniform_limit (sphere z r) f l F"
    4.25 -      and "~ (trivial_limit F)" "0 < r"
    4.26 +      and "\<not> trivial_limit F" "0 < r"
    4.27      shows "l contour_integrable_on (circlepath z r)"
    4.28            "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
    4.29    using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
    4.30 @@ -6550,7 +6550,7 @@
    4.31  lemma holomorphic_uniform_limit:
    4.32    assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
    4.33        and ulim: "uniform_limit (cball z r) f g F"
    4.34 -      and F:  "~ trivial_limit F"
    4.35 +      and F:  "\<not> trivial_limit F"
    4.36    obtains "continuous_on (cball z r) g" "g holomorphic_on ball z r"
    4.37  proof (cases r "0::real" rule: linorder_cases)
    4.38    case less then show ?thesis by (force simp: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that)
    4.39 @@ -6620,7 +6620,7 @@
    4.40    assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
    4.41                                 (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
    4.42        and ulim: "uniform_limit (cball z r) f g F"
    4.43 -      and F:  "~ trivial_limit F" and "0 < r"
    4.44 +      and F:  "\<not> trivial_limit F" and "0 < r"
    4.45    obtains g' where
    4.46        "continuous_on (cball z r) g"
    4.47        "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F"
     5.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Dec 26 20:57:23 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Dec 27 19:48:28 2018 +0100
     5.3 @@ -212,7 +212,7 @@
     5.4  
     5.5  lemma real_lim:
     5.6    fixes l::complex
     5.7 -  assumes "(f \<longlongrightarrow> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
     5.8 +  assumes "(f \<longlongrightarrow> l) F" and "\<not> trivial_limit F" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
     5.9    shows  "l \<in> \<real>"
    5.10  proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
    5.11    show "eventually (\<lambda>x. f x \<in> \<real>) F"
     6.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Dec 26 20:57:23 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Dec 27 19:48:28 2018 +0100
     6.3 @@ -1133,21 +1133,21 @@
     6.4  lemma cnj_tan: "cnj(tan z) = tan(cnj z)"
     6.5    by (simp add: cnj_cos cnj_sin tan_def)
     6.6  
     6.7 -lemma field_differentiable_at_tan: "~(cos z = 0) \<Longrightarrow> tan field_differentiable at z"
     6.8 +lemma field_differentiable_at_tan: "cos z \<noteq> 0 \<Longrightarrow> tan field_differentiable at z"
     6.9    unfolding field_differentiable_def
    6.10    using DERIV_tan by blast
    6.11  
    6.12 -lemma field_differentiable_within_tan: "~(cos z = 0)
    6.13 +lemma field_differentiable_within_tan: "cos z \<noteq> 0
    6.14           \<Longrightarrow> tan field_differentiable (at z within s)"
    6.15    using field_differentiable_at_tan field_differentiable_at_within by blast
    6.16  
    6.17 -lemma continuous_within_tan: "~(cos z = 0) \<Longrightarrow> continuous (at z within s) tan"
    6.18 +lemma continuous_within_tan: "cos z \<noteq> 0 \<Longrightarrow> continuous (at z within s) tan"
    6.19    using continuous_at_imp_continuous_within isCont_tan by blast
    6.20  
    6.21 -lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> continuous_on s tan"
    6.22 +lemma continuous_on_tan [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> cos z \<noteq> 0) \<Longrightarrow> continuous_on s tan"
    6.23    by (simp add: continuous_at_imp_continuous_on)
    6.24  
    6.25 -lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> ~(cos z = 0)) \<Longrightarrow> tan holomorphic_on s"
    6.26 +lemma holomorphic_on_tan: "(\<And>z. z \<in> s \<Longrightarrow> cos z \<noteq> 0) \<Longrightarrow> tan holomorphic_on s"
    6.27    by (simp add: field_differentiable_within_tan holomorphic_on_def)
    6.28  
    6.29  
    6.30 @@ -1670,7 +1670,7 @@
    6.31  
    6.32  lemma Ln_minus:
    6.33    assumes "z \<noteq> 0"
    6.34 -    shows "Ln(-z) = (if Im(z) \<le> 0 \<and> ~(Re(z) < 0 \<and> Im(z) = 0)
    6.35 +    shows "Ln(-z) = (if Im(z) \<le> 0 \<and> \<not>(Re(z) < 0 \<and> Im(z) = 0)
    6.36                       then Ln(z) + \<i> * pi
    6.37                       else Ln(z) - \<i> * pi)" (is "_ = ?rhs")
    6.38    using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
     7.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Wed Dec 26 20:57:23 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Thu Dec 27 19:48:28 2018 +0100
     7.3 @@ -359,7 +359,7 @@
     7.4    assumes holf: "f holomorphic_on S"
     7.5        and S: "open S" and "connected S"
     7.6        and "open U" and "U \<subseteq> S"
     7.7 -      and fne: "~ f constant_on S"
     7.8 +      and fne: "\<not> f constant_on S"
     7.9      shows "open (f ` U)"
    7.10  proof -
    7.11    have *: "open (f ` U)"
    7.12 @@ -468,7 +468,7 @@
    7.13    assumes holf: "f holomorphic_on S"
    7.14        and S: "open S"
    7.15        and "open U" "U \<subseteq> S"
    7.16 -      and fnc: "\<And>X. \<lbrakk>open X; X \<subseteq> S; X \<noteq> {}\<rbrakk> \<Longrightarrow> ~ f constant_on X"
    7.17 +      and fnc: "\<And>X. \<lbrakk>open X; X \<subseteq> S; X \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> f constant_on X"
    7.18      shows "open (f ` U)"
    7.19  proof -
    7.20    have "S = \<Union>(components S)" by simp
    7.21 @@ -518,7 +518,7 @@
    7.22    assume "\<not> f constant_on S"
    7.23    then have "open (f ` U)"
    7.24      using open_mapping_thm assms by blast
    7.25 -  moreover have "~ open (f ` U)"
    7.26 +  moreover have "\<not> open (f ` U)"
    7.27    proof -
    7.28      have "\<exists>t. cmod (f \<xi> - t) < e \<and> t \<notin> f ` U" if "0 < e" for e
    7.29        apply (rule_tac x="if 0 < Re(f \<xi>) then f \<xi> + (e/2) else f \<xi> - (e/2)" in exI)
    7.30 @@ -735,7 +735,7 @@
    7.31  lemma holomorphic_factor_zero_nonconstant:
    7.32    assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
    7.33        and "\<xi> \<in> S" "f \<xi> = 0"
    7.34 -      and nonconst: "~ f constant_on S"
    7.35 +      and nonconst: "\<not> f constant_on S"
    7.36     obtains g r n
    7.37        where "0 < n"  "0 < r"  "ball \<xi> r \<subseteq> S"
    7.38              "g holomorphic_on ball \<xi> r"
    7.39 @@ -1156,7 +1156,7 @@
    7.40    obtain r where "r > 0" "ball \<xi> r \<subseteq> S" "inj_on f (ball \<xi> r)"
    7.41      by (blast intro: that has_complex_derivative_locally_injective [OF assms])
    7.42    then have \<xi>: "\<xi> \<in> ball \<xi> r" by simp
    7.43 -  then have nc: "~ f constant_on ball \<xi> r"
    7.44 +  then have nc: "\<not> f constant_on ball \<xi> r"
    7.45      using \<open>inj_on f (ball \<xi> r)\<close> injective_not_constant by fastforce
    7.46    have holf': "f holomorphic_on ball \<xi> r"
    7.47      using \<open>ball \<xi> r \<subseteq> S\<close> holf holomorphic_on_subset by blast
    7.48 @@ -2132,7 +2132,7 @@
    7.49        case False
    7.50        then have "t > 0"
    7.51          using 2 by (force simp: zero_less_mult_iff)
    7.52 -      have "~ ball a t \<subseteq> s \<Longrightarrow> ball a t \<inter> frontier s \<noteq> {}"
    7.53 +      have "\<not> ball a t \<subseteq> s \<Longrightarrow> ball a t \<inter> frontier s \<noteq> {}"
    7.54          apply (rule connected_Int_frontier [of "ball a t" s], simp_all)
    7.55          using \<open>0 < t\<close> \<open>a \<in> s\<close> centre_in_ball apply blast
    7.56          done
     8.1 --- a/src/HOL/Analysis/Connected.thy	Wed Dec 26 20:57:23 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Connected.thy	Thu Dec 27 19:48:28 2018 +0100
     8.3 @@ -3280,7 +3280,7 @@
     8.4  lemma continuous_on_cases_local:
     8.5       "\<lbrakk>closedin (subtopology euclidean (s \<union> t)) s; closedin (subtopology euclidean (s \<union> t)) t;
     8.6         continuous_on s f; continuous_on t g;
     8.7 -       \<And>x. \<lbrakk>x \<in> s \<and> ~P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
     8.8 +       \<And>x. \<lbrakk>x \<in> s \<and> \<not>P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
     8.9        \<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
    8.10    by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
    8.11  
    8.12 @@ -4983,7 +4983,7 @@
    8.13      shows "connected (S \<union> T)"
    8.14  proof -
    8.15    have *: "\<lbrakk>\<And>x y. P x y \<longleftrightarrow> P y x; \<And>x y. P x y \<Longrightarrow> S \<subseteq> x \<or> S \<subseteq> y;
    8.16 -            \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> ~(\<exists>x y. (P x y))" for P
    8.17 +            \<And>x y. \<lbrakk>P x y; S \<subseteq> x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> \<not>(\<exists>x y. (P x y))" for P
    8.18      by metis
    8.19    show ?thesis
    8.20      unfolding connected_closedin_eq
     9.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Wed Dec 26 20:57:23 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Thu Dec 27 19:48:28 2018 +0100
     9.3 @@ -2,7 +2,7 @@
     9.4      Authors:    LC Paulson, based on material from HOL Light
     9.5  *)
     9.6  
     9.7 -section \<open>Continuous extensions of functions: Urysohn's lemma, Dugundji extension theorem, Tietze\<close>
     9.8 +section \<open>Continuous Extensions of Functions\<close>
     9.9  
    9.10  theory Continuous_Extension
    9.11  imports Starlike
    9.12 @@ -112,7 +112,9 @@
    9.13  qed
    9.14  
    9.15  
    9.16 -subsection\<open>Urysohn's lemma (for Euclidean spaces, where the proof is easy using distances)\<close>
    9.17 +subsection\<open>Urysohn's Lemma for Euclidean Spaces\<close>
    9.18 +
    9.19 +text \<open>For Euclidean spaces the proof is easy using distances.\<close>
    9.20  
    9.21  lemma Urysohn_both_ne:
    9.22    assumes US: "closedin (subtopology euclidean U) S"
    9.23 @@ -130,7 +132,7 @@
    9.24      using \<open>T \<noteq> {}\<close>  UT setdist_eq_0_closedin  by auto
    9.25    have sdpos: "0 < setdist {x} S + setdist {x} T" if "x \<in> U" for x
    9.26    proof -
    9.27 -    have "~ (setdist {x} S = 0 \<and> setdist {x} T = 0)"
    9.28 +    have "\<not> (setdist {x} S = 0 \<and> setdist {x} T = 0)"
    9.29        using assms by (metis IntI empty_iff setdist_eq_0_closedin that)
    9.30      then show ?thesis
    9.31        by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le)
    9.32 @@ -295,7 +297,7 @@
    9.33    using assms by (auto intro: Urysohn_local [of UNIV S T a b])
    9.34  
    9.35  
    9.36 -subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
    9.37 +subsection\<open>The Dugundji Extension Theorem and Tietze Variants\<close>
    9.38  
    9.39  text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
    9.40  https://projecteuclid.org/euclid.pjm/1103052106\<close>
    10.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
    10.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
    10.3 @@ -1343,7 +1343,9 @@
    10.4    by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
    10.5  
    10.6  
    10.7 -subsubsection%unimportant \<open>Some explicit formulations (from Lars Schewe)\<close>
    10.8 +subsubsection%unimportant \<open>Some explicit formulations\<close>
    10.9 +
   10.10 +text "Formalized by Lars Schewe."
   10.11  
   10.12  lemma affine:
   10.13    fixes V::"'a::real_vector set"
   10.14 @@ -2070,7 +2072,9 @@
   10.15  qed
   10.16  
   10.17  
   10.18 -subsection \<open>Affine dependence and consequential theorems (from Lars Schewe)\<close>
   10.19 +subsection \<open>Affine dependence and consequential theorems\<close>
   10.20 +
   10.21 +text "Formalized by Lars Schewe."
   10.22  
   10.23  definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
   10.24    where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
   10.25 @@ -2082,11 +2086,11 @@
   10.26  done
   10.27  
   10.28  lemma affine_independent_subset:
   10.29 -  shows "\<lbrakk>~ affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> ~ affine_dependent s"
   10.30 +  shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
   10.31  by (metis affine_dependent_subset)
   10.32  
   10.33  lemma affine_independent_Diff:
   10.34 -   "~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
   10.35 +   "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
   10.36  by (meson Diff_subset affine_dependent_subset)
   10.37  
   10.38  proposition affine_dependent_explicit:
   10.39 @@ -2601,7 +2605,9 @@
   10.40  qed (use assms in \<open>auto simp: convex_explicit\<close>)
   10.41  
   10.42  
   10.43 -subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
   10.44 +subsubsection%unimportant \<open>Another formulation\<close>
   10.45 +
   10.46 +text "Formalized by Lars Schewe."
   10.47  
   10.48  lemma convex_hull_explicit:
   10.49    fixes p :: "'a::real_vector set"
   10.50 @@ -3427,7 +3433,7 @@
   10.51  
   10.52  lemma affine_independent_iff_card:
   10.53      fixes s :: "'a::euclidean_space set"
   10.54 -    shows "~ affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
   10.55 +    shows "\<not> affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
   10.56    apply (rule iffI)
   10.57    apply (simp add: aff_dim_affine_independent aff_independent_finite)
   10.58    by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
   10.59 @@ -3652,7 +3658,7 @@
   10.60  
   10.61  lemma affine_independent_card_dim_diffs:
   10.62    fixes S :: "'a :: euclidean_space set"
   10.63 -  assumes "~ affine_dependent S" "a \<in> S"
   10.64 +  assumes "\<not> affine_dependent S" "a \<in> S"
   10.65      shows "card S = dim {x - a|x. x \<in> S} + 1"
   10.66  proof -
   10.67    have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
   10.68 @@ -3766,7 +3772,7 @@
   10.69    show ?thesis
   10.70    proof safe
   10.71      assume 0: "aff_dim S = 0"
   10.72 -    have "~ {a,b} \<subseteq> S" if "b \<noteq> a" for b
   10.73 +    have "\<not> {a,b} \<subseteq> S" if "b \<noteq> a" for b
   10.74        by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
   10.75      then show "\<exists>a. S = {a}"
   10.76        using \<open>a \<in> S\<close> by blast
   10.77 @@ -3798,7 +3804,7 @@
   10.78  
   10.79  lemma disjoint_affine_hull:
   10.80    fixes s :: "'n::euclidean_space set"
   10.81 -  assumes "~ affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
   10.82 +  assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
   10.83      shows "(affine hull t) \<inter> (affine hull u) = {}"
   10.84  proof -
   10.85    have "finite s" using assms by (simp add: aff_independent_finite)
   10.86 @@ -3813,7 +3819,7 @@
   10.87      have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u" using assms by auto
   10.88      have "sum c s = 0"
   10.89        by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
   10.90 -    moreover have "~ (\<forall>v\<in>s. c v = 0)"
   10.91 +    moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
   10.92        by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum_not_0 zero_neq_one)
   10.93      moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
   10.94        by (simp add: c_def if_smult sum_negf
   10.95 @@ -5747,7 +5753,9 @@
   10.96  qed auto
   10.97  
   10.98  
   10.99 -subsection \<open>Radon's theorem (from Lars Schewe)\<close>
  10.100 +subsection \<open>Radon's theorem\<close>
  10.101 +
  10.102 +text "Formalized by Lars Schewe."
  10.103  
  10.104  lemma radon_ex_lemma:
  10.105    assumes "finite c" "affine_dependent c"
    11.1 --- a/src/HOL/Analysis/Cross3.thy	Wed Dec 26 20:57:23 2018 +0100
    11.2 +++ b/src/HOL/Analysis/Cross3.thy	Thu Dec 27 19:48:28 2018 +0100
    11.3 @@ -99,7 +99,7 @@
    11.4    by (force simp add: axis_def cross3_simps)+
    11.5  
    11.6  lemma  cross_basis_nonzero:
    11.7 -  "u \<noteq> 0 \<Longrightarrow> ~(u \<times> axis 1 1 = 0) \<or> ~(u \<times> axis 2 1 = 0) \<or> ~(u \<times> axis 3 1 = 0)"
    11.8 +  "u \<noteq> 0 \<Longrightarrow> u \<times> axis 1 1 \<noteq> 0 \<or> u \<times> axis 2 1 \<noteq> 0 \<or> u \<times> axis 3 1 \<noteq> 0"
    11.9    by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
   11.10  
   11.11  lemma  cross_dot_cancel:
    12.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Dec 26 20:57:23 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Dec 27 19:48:28 2018 +0100
    12.3 @@ -1195,8 +1195,8 @@
    12.4    proof (rule starlike_negligible [OF \<open>closed S\<close>, of a])
    12.5      fix c x
    12.6      assume cx: "a + c *\<^sub>R x \<in> S" "0 \<le> c" "a + x \<in> S"
    12.7 -    with star have "~ (c < 1)" by auto
    12.8 -    moreover have "~ (c > 1)"
    12.9 +    with star have "\<not> (c < 1)" by auto
   12.10 +    moreover have "\<not> (c > 1)"
   12.11        using star [of "1/c" "c *\<^sub>R x"] cx by force
   12.12      ultimately show "c = 1" by arith
   12.13    qed
    13.1 --- a/src/HOL/Analysis/Further_Topology.thy	Wed Dec 26 20:57:23 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Thu Dec 27 19:48:28 2018 +0100
    13.3 @@ -366,7 +366,7 @@
    13.4        by (meson f nullhomotopic_from_contractible contractible_sphere that)
    13.5    next
    13.6      case False
    13.7 -    with \<open>~ s \<le> 0\<close> have "r > 0" "s > 0" by auto
    13.8 +    with \<open>\<not> s \<le> 0\<close> have "r > 0" "s > 0" by auto
    13.9      show ?thesis
   13.10        apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f])
   13.11        using  \<open>0 < r\<close> \<open>0 < s\<close> assms(1)
   13.12 @@ -414,7 +414,7 @@
   13.13    assumes fin: "finite \<F>"
   13.14        and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
   13.15        and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
   13.16 -      and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; ~ X \<subseteq> Y; ~ Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
   13.17 +      and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
   13.18      shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
   13.19  apply (simp add: Union_maximal_sets [OF fin, symmetric])
   13.20  apply (rule extending_maps_Union_aux)
   13.21 @@ -567,7 +567,7 @@
   13.22      have clo: "closed S" if "S \<in> \<G> \<union> ?Faces" for S
   13.23        using that \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly polytope_imp_closed by blast
   13.24      have K: "X \<inter> Y \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int p})"
   13.25 -                if "X \<in> \<G> \<union> ?Faces" "Y \<in> \<G> \<union> ?Faces" "~ Y \<subseteq> X" for X Y
   13.26 +                if "X \<in> \<G> \<union> ?Faces" "Y \<in> \<G> \<union> ?Faces" "\<not> Y \<subseteq> X" for X Y
   13.27      proof -
   13.28        have ff: "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
   13.29          if XY: "X face_of D" "Y face_of E" and DE: "D \<in> \<F>" "E \<in> \<F>" for D E
   13.30 @@ -669,7 +669,7 @@
   13.31  assumes "finite \<F>"
   13.32      and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g ` (X - {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
   13.33      and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
   13.34 -    and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; ~(X \<subseteq> Y); ~(Y \<subseteq> X)\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
   13.35 +    and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
   13.36    obtains C g where "finite C" "disjnt C U" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
   13.37                      "g ` (\<Union>\<F> - C) \<subseteq> T"
   13.38                      "\<And>x. x \<in> (\<Union>\<F> - C) \<inter> K \<Longrightarrow> g x = h x"
   13.39 @@ -1188,8 +1188,8 @@
   13.40      then have "ball a d \<inter> U \<subseteq> C"
   13.41        by auto
   13.42      obtain h k where homhk: "homeomorphism (S \<union> C) (S \<union> C) h k"
   13.43 -                 and subC: "{x. (~ (h x = x \<and> k x = x))} \<subseteq> C"
   13.44 -                 and bou: "bounded {x. (~ (h x = x \<and> k x = x))}"
   13.45 +                 and subC: "{x. (\<not> (h x = x \<and> k x = x))} \<subseteq> C"
   13.46 +                 and bou: "bounded {x. (\<not> (h x = x \<and> k x = x))}"
   13.47                   and hin: "\<And>x. x \<in> C \<inter> K \<Longrightarrow> h x \<in> ball a d \<inter> U"
   13.48      proof (rule homeomorphism_grouping_points_exists_gen [of C "ball a d \<inter> U" "C \<inter> K" "S \<union> C"])
   13.49        show "openin (subtopology euclidean C) (ball a d \<inter> U)"
   13.50 @@ -1539,7 +1539,7 @@
   13.51      by (simp add: assms compact_imp_bounded)
   13.52    then obtain b where b: "S \<subseteq> cbox (-b) b"
   13.53      using bounded_subset_cbox_symmetric by blast
   13.54 -  define LU where "LU \<equiv> L \<union> (\<Union> {C \<in> components (T - S). ~bounded C} - cbox (-(b+One)) (b+One))"
   13.55 +  define LU where "LU \<equiv> L \<union> (\<Union> {C \<in> components (T - S). \<not>bounded C} - cbox (-(b+One)) (b+One))"
   13.56    obtain K g where "finite K" "K \<subseteq> LU" "K \<subseteq> T" "disjnt K S"
   13.57                 and contg: "continuous_on (T - K) g"
   13.58                 and gim: "g ` (T - K) \<subseteq> rel_frontier U"
   13.59 @@ -1699,7 +1699,7 @@
   13.60  theorem%important Borsuk_separation_theorem_gen:
   13.61    fixes S :: "'a::euclidean_space set"
   13.62    assumes "compact S"
   13.63 -    shows "(\<forall>c \<in> components(- S). ~bounded c) \<longleftrightarrow>
   13.64 +    shows "(\<forall>c \<in> components(- S). \<not>bounded c) \<longleftrightarrow>
   13.65             (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
   13.66                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
   13.67         (is "?lhs = ?rhs")
   13.68 @@ -5204,7 +5204,7 @@
   13.69  proof (rule ccontr)
   13.70    let ?S = "S \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> S}"
   13.71    let ?T = "T \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> T}"
   13.72 -  assume "~ thesis"
   13.73 +  assume "\<not> thesis"
   13.74    with that have *: "frontier C \<inter> S = {} \<or> frontier C \<inter> T = {}"
   13.75              if C: "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
   13.76      using C by blast
    14.1 --- a/src/HOL/Analysis/Great_Picard.thy	Wed Dec 26 20:57:23 2018 +0100
    14.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Thu Dec 27 19:48:28 2018 +0100
    14.3 @@ -874,7 +874,7 @@
    14.4             have le_er: "cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) \<le> e / r"
    14.5                  if "cmod (x - z) = r/3 + r/3" for x
    14.6             proof -
    14.7 -             have "~ (cmod (x - y) < r/3)"
    14.8 +             have "\<not> (cmod (x - y) < r/3)"
    14.9                 using y_near_z(1) that \<open>M > 0\<close> \<open>r > 0\<close>
   14.10                 by (metis (full_types) norm_diff_triangle_less norm_minus_commute order_less_irrefl)
   14.11               then have r4_le_xy: "r/4 \<le> cmod (x - y)"
   14.12 @@ -1000,7 +1000,7 @@
   14.13        and holf: "\<And>n::nat. \<F> n holomorphic_on S"
   14.14        and holg: "g holomorphic_on S"
   14.15        and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
   14.16 -      and nonconst: "~ g constant_on S"
   14.17 +      and nonconst: "\<not> g constant_on S"
   14.18        and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
   14.19        and "z0 \<in> S"
   14.20        shows "g z0 \<noteq> 0"
   14.21 @@ -1164,7 +1164,7 @@
   14.22        and holf: "\<And>n::nat. \<F> n holomorphic_on S"
   14.23        and holg: "g holomorphic_on S"
   14.24        and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
   14.25 -      and nonconst: "~ g constant_on S"
   14.26 +      and nonconst: "\<not> g constant_on S"
   14.27        and inj: "\<And>n. inj_on (\<F> n) S"
   14.28      shows "inj_on g S"
   14.29  proof%unimportant -
   14.30 @@ -1309,7 +1309,7 @@
   14.31        unfolding open_subopen [of U] by (auto simp: U_def)
   14.32      fix v
   14.33      assume v: "v islimpt U" "v \<in> S"
   14.34 -    have "~ (\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v))"
   14.35 +    have "\<not> (\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v))"
   14.36      proof
   14.37        assume "\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v)"
   14.38        then have "\<forall>n. \<exists>h\<in>Y. Suc n < cmod (h v)"
    15.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Dec 26 20:57:23 2018 +0100
    15.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 19:48:28 2018 +0100
    15.3 @@ -79,7 +79,7 @@
    15.4  lemma content_pos_le [iff]: "0 \<le> content X"
    15.5    by simp
    15.6  
    15.7 -corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
    15.8 +corollary content_nonneg [simp]: "\<not> content (cbox a b) < 0"
    15.9    using not_le by blast
   15.10  
   15.11  lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
   15.12 @@ -287,12 +287,12 @@
   15.13  definition integrable_on (infixr "integrable'_on" 46)
   15.14    where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
   15.15  
   15.16 -definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
   15.17 +definition "integral i f = (SOME y. (f has_integral y) i \<or> \<not> f integrable_on i \<and> y=0)"
   15.18  
   15.19  lemma integrable_integral[intro]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
   15.20    unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
   15.21  
   15.22 -lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
   15.23 +lemma not_integrable_integral: "\<not> f integrable_on i \<Longrightarrow> integral i f = 0"
   15.24    unfolding integrable_on_def integral_def by blast
   15.25  
   15.26  lemma has_integral_integrable[dest]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
   15.27 @@ -356,7 +356,7 @@
   15.28  lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
   15.29    by blast
   15.30  
   15.31 -lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> ~ f integrable_on k \<and> y=0"
   15.32 +lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> \<not> f integrable_on k \<and> y=0"
   15.33    unfolding integral_def integrable_on_def
   15.34    apply (erule subst)
   15.35    apply (rule someI_ex)
   15.36 @@ -498,7 +498,7 @@
   15.37    case True then show ?thesis
   15.38      by (force intro: has_integral_mult_left)
   15.39  next
   15.40 -  case False then have "~ (\<lambda>x. f x * c) integrable_on S"
   15.41 +  case False then have "\<not> (\<lambda>x. f x * c) integrable_on S"
   15.42      using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ S "inverse c"]
   15.43      by (auto simp add: mult.assoc)
   15.44    with False show ?thesis by (simp add: not_integrable_integral)
   15.45 @@ -615,7 +615,7 @@
   15.46    case True with has_integral_cmul integrable_integral show ?thesis
   15.47      by fastforce
   15.48  next
   15.49 -  case False then have "~ (\<lambda>x. c *\<^sub>R f x) integrable_on S"
   15.50 +  case False then have "\<not> (\<lambda>x. c *\<^sub>R f x) integrable_on S"
   15.51      using has_integral_cmul [of "(\<lambda>x. c *\<^sub>R f x)" _ S "inverse c"] by auto
   15.52    with False show ?thesis by (simp add: not_integrable_integral)
   15.53  qed
   15.54 @@ -630,7 +630,7 @@
   15.55    case True then show ?thesis
   15.56      by (simp add: has_integral_neg integrable_integral integral_unique)
   15.57  next
   15.58 -  case False then have "~ (\<lambda>x. - f x) integrable_on S"
   15.59 +  case False then have "\<not> (\<lambda>x. - f x) integrable_on S"
   15.60      using has_integral_neg [of "(\<lambda>x. - f x)" _ S ] by auto
   15.61    with False show ?thesis by (simp add: not_integrable_integral)
   15.62  qed
    16.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Wed Dec 26 20:57:23 2018 +0100
    16.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Dec 27 19:48:28 2018 +0100
    16.3 @@ -201,7 +201,7 @@
    16.4  lemma%unimportant segment_to_rel_frontier:
    16.5    fixes x :: "'a::euclidean_space"
    16.6    assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
    16.7 -      and y: "y \<in> S" and xy: "~(x = y \<and> S = {x})"
    16.8 +      and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
    16.9    obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
   16.10                    "open_segment x z \<subseteq> rel_interior S"
   16.11  proof (cases "x=y")
    17.1 --- a/src/HOL/Analysis/Improper_Integral.thy	Wed Dec 26 20:57:23 2018 +0100
    17.2 +++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Dec 27 19:48:28 2018 +0100
    17.3 @@ -924,7 +924,7 @@
    17.4            moreover have "norm (\<Sum>(x,K) \<in> T'. ?CI K h x - ?CI K f x)
    17.5                  \<le> 2*\<epsilon>/3"
    17.6            proof -
    17.7 -            define T'' where "T'' \<equiv> {(x,K) \<in> T'. ~ (K \<subseteq> {x. x \<bullet> i \<le> c})}"
    17.8 +            define T'' where "T'' \<equiv> {(x,K) \<in> T'. \<not> (K \<subseteq> {x. x \<bullet> i \<le> c})}"
    17.9              then have "T'' \<subseteq> T'"
   17.10                by auto
   17.11              then have "finite T''"
    18.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Wed Dec 26 20:57:23 2018 +0100
    18.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Thu Dec 27 19:48:28 2018 +0100
    18.3 @@ -374,7 +374,7 @@
    18.4        qed
    18.5        then have "connected_component (- (path_image u \<union> path_image d \<union> path_image g)) x y"
    18.6          by (simp add: Un_ac)
    18.7 -      moreover have "~(connected_component (- (path_image c)) x y)"
    18.8 +      moreover have "\<not>(connected_component (- (path_image c)) x y)"
    18.9          by (metis (no_types, lifting) \<open>\<not> bounded outer\<close> \<open>bounded inner\<close> \<open>x \<in> inner\<close> \<open>y \<in> outer\<close> componentsE connected_component_eq inner mem_Collect_eq outer)
   18.10        ultimately show False
   18.11          by (auto simp: ud_Un [symmetric] connected_component_def)
    19.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
    19.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
    19.3 @@ -145,7 +145,7 @@
    19.4  qed
    19.5  
    19.6  lemma%unimportant (in order) atLeastatMost_empty'[simp]:
    19.7 -  "(~ a <= b) \<Longrightarrow> {a..b} = {}"
    19.8 +  "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
    19.9    by (auto)
   19.10  
   19.11  instance real :: ordered_euclidean_space
    20.1 --- a/src/HOL/Analysis/Path_Connected.thy	Wed Dec 26 20:57:23 2018 +0100
    20.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 27 19:48:28 2018 +0100
    20.3 @@ -591,7 +591,7 @@
    20.4      using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
    20.5    have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
    20.6      using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
    20.7 -  have [simp]: "~ min (1 / 2) (min d1 d2) \<le> 0"
    20.8 +  have [simp]: "\<not> min (1 / 2) (min d1 d2) \<le> 0"
    20.9      using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
   20.10    have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
   20.11         "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
   20.12 @@ -670,7 +670,7 @@
   20.13    have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u
   20.14      using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>]
   20.15      by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps)
   20.16 -  then have n1: "~ (pathstart g1 \<in> path_image g2)"
   20.17 +  then have n1: "pathstart g1 \<notin> path_image g2"
   20.18      unfolding pathstart_def path_image_def
   20.19      using atLeastAtMost_iff by blast
   20.20    show ?rhs using \<open>?lhs\<close>
   20.21 @@ -2442,7 +2442,7 @@
   20.22  lemma cobounded_unbounded_component:
   20.23      fixes s :: "'a :: euclidean_space set"
   20.24      assumes "bounded (-s)"
   20.25 -      shows "\<exists>x. x \<in> s \<and> ~ bounded (connected_component_set s x)"
   20.26 +      shows "\<exists>x. x \<in> s \<and> \<not> bounded (connected_component_set s x)"
   20.27  proof -
   20.28    obtain i::'a where i: "i \<in> Basis"
   20.29      using nonempty_Basis by blast
   20.30 @@ -2450,7 +2450,7 @@
   20.31      using bounded_subset_ballD [OF assms, of 0] by auto
   20.32    then have *: "\<And>x. B \<le> norm x \<Longrightarrow> x \<in> s"
   20.33      by (force simp: ball_def dist_norm)
   20.34 -  have unbounded_inner: "~ bounded {x. inner i x \<ge> B}"
   20.35 +  have unbounded_inner: "\<not> bounded {x. inner i x \<ge> B}"
   20.36      apply (auto simp: bounded_def dist_norm)
   20.37      apply (rule_tac x="x + (max B e + 1 + \<bar>i \<bullet> x\<bar>) *\<^sub>R i" in exI)
   20.38      apply simp
   20.39 @@ -2475,8 +2475,8 @@
   20.40  lemma cobounded_unique_unbounded_component:
   20.41      fixes s :: "'a :: euclidean_space set"
   20.42      assumes bs: "bounded (-s)" and "2 \<le> DIM('a)"
   20.43 -        and bo: "~ bounded(connected_component_set s x)"
   20.44 -                "~ bounded(connected_component_set s y)"
   20.45 +        and bo: "\<not> bounded(connected_component_set s x)"
   20.46 +                "\<not> bounded(connected_component_set s y)"
   20.47        shows "connected_component_set s x = connected_component_set s y"
   20.48  proof -
   20.49    obtain i::'a where i: "i \<in> Basis"
   20.50 @@ -2507,7 +2507,7 @@
   20.51  
   20.52  lemma cobounded_unbounded_components:
   20.53      fixes s :: "'a :: euclidean_space set"
   20.54 -    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> ~bounded c"
   20.55 +    shows "bounded (-s) \<Longrightarrow> \<exists>c. c \<in> components s \<and> \<not>bounded c"
   20.56    by (metis cobounded_unbounded_component components_def imageI)
   20.57  
   20.58  lemma cobounded_unique_unbounded_components:
   20.59 @@ -2532,9 +2532,9 @@
   20.60    "inside S \<equiv> {x. (x \<notin> S) \<and> bounded(connected_component_set ( - S) x)}"
   20.61  
   20.62  definition%important outside where
   20.63 -  "outside S \<equiv> -S \<inter> {x. ~ bounded(connected_component_set (- S) x)}"
   20.64 -
   20.65 -lemma outside: "outside S = {x. ~ bounded(connected_component_set (- S) x)}"
   20.66 +  "outside S \<equiv> -S \<inter> {x. \<not> bounded(connected_component_set (- S) x)}"
   20.67 +
   20.68 +lemma outside: "outside S = {x. \<not> bounded(connected_component_set (- S) x)}"
   20.69    by (auto simp: outside_def) (metis Compl_iff bounded_empty connected_component_eq_empty)
   20.70  
   20.71  lemma inside_no_overlap [simp]: "inside S \<inter> S = {}"
   20.72 @@ -2619,7 +2619,7 @@
   20.73  
   20.74  lemma unbounded_outside:
   20.75      fixes S :: "'a::{real_normed_vector, perfect_space} set"
   20.76 -    shows "bounded S \<Longrightarrow> ~ bounded(outside S)"
   20.77 +    shows "bounded S \<Longrightarrow> \<not> bounded(outside S)"
   20.78    using cobounded_imp_unbounded cobounded_outside by blast
   20.79  
   20.80  lemma bounded_inside:
   20.81 @@ -2655,7 +2655,7 @@
   20.82  lemma not_outside_connected_component_lt:
   20.83      fixes S :: "'a::euclidean_space set"
   20.84      assumes S: "bounded S" and "2 \<le> DIM('a)"
   20.85 -      shows "- (outside S) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> ~ (connected_component (- S) x y)}"
   20.86 +      shows "- (outside S) = {x. \<forall>B. \<exists>y. B < norm(y) \<and> \<not> connected_component (- S) x y}"
   20.87  proof -
   20.88    obtain B::real where B: "0 < B" and Bno: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
   20.89      using S [simplified bounded_pos] by auto
   20.90 @@ -2681,24 +2681,24 @@
   20.91  lemma not_outside_connected_component_le:
   20.92      fixes S :: "'a::euclidean_space set"
   20.93      assumes S: "bounded S"  "2 \<le> DIM('a)"
   20.94 -      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> ~ (connected_component (- S) x y)}"
   20.95 +      shows "- (outside S) = {x. \<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y}"
   20.96  apply (auto intro: less_imp_le simp: not_outside_connected_component_lt [OF assms])
   20.97  by (meson gt_ex less_le_trans)
   20.98  
   20.99  lemma inside_connected_component_lt:
  20.100      fixes S :: "'a::euclidean_space set"
  20.101      assumes S: "bounded S"  "2 \<le> DIM('a)"
  20.102 -      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> ~(connected_component (- S) x y))}"
  20.103 +      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B < norm(y) \<and> \<not> connected_component (- S) x y)}"
  20.104    by (auto simp: inside_outside not_outside_connected_component_lt [OF assms])
  20.105  
  20.106  lemma inside_connected_component_le:
  20.107      fixes S :: "'a::euclidean_space set"
  20.108      assumes S: "bounded S"  "2 \<le> DIM('a)"
  20.109 -      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> ~(connected_component (- S) x y))}"
  20.110 +      shows "inside S = {x. (x \<notin> S) \<and> (\<forall>B. \<exists>y. B \<le> norm(y) \<and> \<not> connected_component (- S) x y)}"
  20.111    by (auto simp: inside_outside not_outside_connected_component_le [OF assms])
  20.112  
  20.113  lemma inside_subset:
  20.114 -  assumes "connected U" and "~bounded U" and "T \<union> U = - S"
  20.115 +  assumes "connected U" and "\<not> bounded U" and "T \<union> U = - S"
  20.116    shows "inside S \<subseteq> T"
  20.117  apply (auto simp: inside_def)
  20.118  by (metis bounded_subset [of "connected_component_set (- S) _"] connected_component_maximal
  20.119 @@ -2794,7 +2794,7 @@
  20.120  lemma frontier_minimal_separating_closed:
  20.121    fixes S :: "'a::real_normed_vector set"
  20.122    assumes "closed S"
  20.123 -      and nconn: "~ connected(- S)"
  20.124 +      and nconn: "\<not> connected(- S)"
  20.125        and C: "C \<in> components (- S)"
  20.126        and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected(- T)"
  20.127      shows "frontier C = S"
  20.128 @@ -3319,7 +3319,7 @@
  20.129  
  20.130  lemma bounded_unique_outside:
  20.131      fixes s :: "'a :: euclidean_space set"
  20.132 -    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> ~bounded c \<longleftrightarrow> c = outside s)"
  20.133 +    shows "\<lbrakk>bounded s; DIM('a) \<ge> 2\<rbrakk> \<Longrightarrow> (c \<in> components (- s) \<and> \<not> bounded c \<longleftrightarrow> c = outside s)"
  20.134    apply (rule iffI)
  20.135    apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
  20.136    by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
  20.137 @@ -3365,7 +3365,7 @@
  20.138        apply (rule le_no)
  20.139        using w wy oint
  20.140        by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
  20.141 -    have **: "(~(b \<inter> (- S) = {}) \<and> ~(b - (- S) = {}) \<Longrightarrow> (b \<inter> f \<noteq> {}))
  20.142 +    have **: "(b \<inter> (- S) \<noteq> {} \<and> b - (- S) \<noteq> {} \<Longrightarrow> b \<inter> f \<noteq> {})
  20.143                \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
  20.144                b \<subseteq> S" for b f and S :: "'b set"
  20.145        by blast
  20.146 @@ -5065,7 +5065,7 @@
  20.147      done
  20.148  qed
  20.149  
  20.150 -subsection\<open>Sort of induction principle for connected sets\<close>
  20.151 +subsection\<open>An induction principle for connected sets\<close>
  20.152  
  20.153  proposition connected_induction:
  20.154    assumes "connected S"
  20.155 @@ -5084,7 +5084,7 @@
  20.156      done
  20.157    have 2: "openin (subtopology euclidean S)
  20.158               {b. \<exists>T. openin (subtopology euclidean S) T \<and>
  20.159 -                     b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> ~ Q x)}"
  20.160 +                     b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
  20.161      apply (subst openin_subopen, clarify)
  20.162      apply (rule_tac x=T in exI, auto)
  20.163      done
  20.164 @@ -5742,7 +5742,7 @@
  20.165  qed blast
  20.166  
  20.167  
  20.168 -subsection\<open>Important special cases of local connectedness and path connectedness\<close>
  20.169 +subsection\<open>Special cases of local connectedness and path connectedness\<close>
  20.170  
  20.171  lemma locally_connected_1:
  20.172    assumes
  20.173 @@ -7155,7 +7155,7 @@
  20.174  
  20.175  lemma connected_card_eq_iff_nontrivial:
  20.176    fixes S :: "'a::metric_space set"
  20.177 -  shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> ~(\<exists>a. S \<subseteq> {a})"
  20.178 +  shows "connected S \<Longrightarrow> uncountable S \<longleftrightarrow> \<not>(\<exists>a. S \<subseteq> {a})"
  20.179    apply (auto simp: countable_finite finite_subset)
  20.180    by (metis connected_uncountable is_singletonI' is_singleton_the_elem subset_singleton_iff)
  20.181  
  20.182 @@ -7184,7 +7184,7 @@
  20.183  
  20.184  proposition path_connected_convex_diff_countable:
  20.185    fixes U :: "'a::euclidean_space set"
  20.186 -  assumes "convex U" "~ collinear U" "countable S"
  20.187 +  assumes "convex U" "\<not> collinear U" "countable S"
  20.188      shows "path_connected(U - S)"
  20.189  proof (clarsimp simp add: path_connected_def)
  20.190    fix a b
  20.191 @@ -7202,7 +7202,7 @@
  20.192      have "?m \<in> U"
  20.193        using \<open>a \<in> U\<close> \<open>b \<in> U\<close> \<open>convex U\<close> convex_contains_segment by force
  20.194      obtain c where "c \<in> U" and nc_abc: "\<not> collinear {a,b,c}"
  20.195 -      by (metis False \<open>a \<in> U\<close> \<open>b \<in> U\<close> \<open>~ collinear U\<close> collinear_triples insert_absorb)
  20.196 +      by (metis False \<open>a \<in> U\<close> \<open>b \<in> U\<close> \<open>\<not> collinear U\<close> collinear_triples insert_absorb)
  20.197      have ncoll_mca: "\<not> collinear {?m,c,a}"
  20.198        by (metis (full_types) \<open>a \<noteq> ?m\<close> collinear_3_trans collinear_midpoint insert_commute nc_abc)
  20.199      have ncoll_mcb: "\<not> collinear {?m,c,b}"
  20.200 @@ -7289,7 +7289,7 @@
  20.201  
  20.202  corollary connected_convex_diff_countable:
  20.203    fixes U :: "'a::euclidean_space set"
  20.204 -  assumes "convex U" "~ collinear U" "countable S"
  20.205 +  assumes "convex U" "\<not> collinear U" "countable S"
  20.206    shows "connected(U - S)"
  20.207    by (simp add: assms path_connected_convex_diff_countable path_connected_imp_connected)
  20.208  
  20.209 @@ -7344,7 +7344,7 @@
  20.210  proposition path_connected_openin_diff_countable:
  20.211    fixes S :: "'a::euclidean_space set"
  20.212    assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S"
  20.213 -      and "~ collinear S" "countable T"
  20.214 +      and "\<not> collinear S" "countable T"
  20.215      shows "path_connected(S - T)"
  20.216  proof (clarsimp simp add: path_connected_component)
  20.217    fix x y
  20.218 @@ -7360,8 +7360,8 @@
  20.219          by (auto simp: openin_contains_ball)
  20.220        with \<open>x \<in> U\<close> have x: "x \<in> ball x r \<inter> affine hull S"
  20.221          by auto
  20.222 -      have "~ S \<subseteq> {x}"
  20.223 -        using \<open>~ collinear S\<close>  collinear_subset by blast
  20.224 +      have "\<not> S \<subseteq> {x}"
  20.225 +        using \<open>\<not> collinear S\<close>  collinear_subset by blast
  20.226        then obtain x' where "x' \<noteq> x" "x' \<in> S"
  20.227          by blast
  20.228        obtain y where y: "y \<noteq> x" "y \<in> ball x r \<inter> affine hull S"
  20.229 @@ -7414,7 +7414,7 @@
  20.230  corollary connected_openin_diff_countable:
  20.231    fixes S :: "'a::euclidean_space set"
  20.232    assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S"
  20.233 -      and "~ collinear S" "countable T"
  20.234 +      and "\<not> collinear S" "countable T"
  20.235      shows "connected(S - T)"
  20.236    by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms])
  20.237  
  20.238 @@ -7445,7 +7445,7 @@
  20.239  
  20.240  
  20.241  
  20.242 -subsection\<open>Self-homeomorphisms shuffling points about in various ways\<close>
  20.243 +subsection\<open>Self-homeomorphisms shuffling points about\<close>
  20.244  
  20.245  subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
  20.246  
  20.247 @@ -7610,7 +7610,7 @@
  20.248    assumes "affine T" "a \<in> T" and ST: "ball a r \<inter> T \<subseteq> S" "S \<subseteq> T"
  20.249        and u: "u \<in> ball a r \<inter> T" and v: "v \<in> ball a r \<inter> T"
  20.250    obtains f g where "homeomorphism S S f g"
  20.251 -                    "f u = v" "{x. ~ (f x = x \<and> g x = x)} \<subseteq> ball a r \<inter> T"
  20.252 +                    "f u = v" "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> ball a r \<inter> T"
  20.253  proof -
  20.254    obtain f g where hom: "homeomorphism (cball a r \<inter> T) (cball a r \<inter> T) f g"
  20.255                 and "f u = v" and fid: "\<And>x. \<lbrakk>x \<in> sphere a r; x \<in> T\<rbrakk> \<Longrightarrow> f x = x"
  20.256 @@ -7690,14 +7690,14 @@
  20.257        and TS: "T \<subseteq> affine hull S"
  20.258        and S: "connected S" "a \<in> S" "b \<in> S"
  20.259    obtains f g where "homeomorphism T T f g" "f a = b"
  20.260 -                    "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S"
  20.261 -                    "bounded {x. ~ (f x = x \<and> g x = x)}"
  20.262 +                    "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S"
  20.263 +                    "bounded {x. \<not> (f x = x \<and> g x = x)}"
  20.264  proof -
  20.265    have 1: "\<exists>h k. homeomorphism T T h k \<and> h (f d) = d \<and>
  20.266 -              {x. ~ (h x = x \<and> k x = x)} \<subseteq> S \<and> bounded {x. ~ (h x = x \<and> k x = x)}"
  20.267 +              {x. \<not> (h x = x \<and> k x = x)} \<subseteq> S \<and> bounded {x. \<not> (h x = x \<and> k x = x)}"
  20.268          if "d \<in> S" "f d \<in> S" and homfg: "homeomorphism T T f g"
  20.269 -        and S: "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S"
  20.270 -        and bo: "bounded {x. ~ (f x = x \<and> g x = x)}" for d f g
  20.271 +        and S: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S"
  20.272 +        and bo: "bounded {x. \<not> (f x = x \<and> g x = x)}" for d f g
  20.273    proof (intro exI conjI)
  20.274      show homgf: "homeomorphism T T g f"
  20.275        by (metis homeomorphism_symD homfg)
  20.276 @@ -7722,7 +7722,7 @@
  20.277        by force
  20.278      show "{x. \<not> ((f2 \<circ> f1) x = x \<and> (g1 \<circ> g2) x = x)} \<subseteq> S"
  20.279        using sub by force
  20.280 -    have "bounded ({x. ~(f1 x = x \<and> g1 x = x)} \<union> {x. ~(f2 x = x \<and> g2 x = x)})"
  20.281 +    have "bounded ({x. \<not>(f1 x = x \<and> g1 x = x)} \<union> {x. \<not>(f2 x = x \<and> g2 x = x)})"
  20.282        using bo by simp
  20.283      then show "bounded {x. \<not> ((f2 \<circ> f1) x = x \<and> (g1 \<circ> g2) x = x)}"
  20.284        by (rule bounded_subset) auto
  20.285 @@ -7753,7 +7753,7 @@
  20.286        done
  20.287    qed
  20.288    have "\<exists>f g. homeomorphism T T f g \<and> f a = b \<and>
  20.289 -              {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
  20.290 +              {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
  20.291      apply (rule connected_equivalence_relation [OF S], safe)
  20.292        apply (blast intro: 1 2 3)+
  20.293      done
  20.294 @@ -7769,7 +7769,7 @@
  20.295        and ope: "openin (subtopology euclidean (affine hull S)) S"
  20.296        and "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
  20.297    shows "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(x i) = y i) \<and>
  20.298 -               {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
  20.299 +               {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
  20.300    using assms
  20.301  proof (induction K)
  20.302    case empty
  20.303 @@ -7783,11 +7783,11 @@
  20.304         and xyS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
  20.305      by (simp_all add: pairwise_insert)
  20.306    obtain f g where homfg: "homeomorphism T T f g" and feq: "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
  20.307 -               and fg_sub: "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S"
  20.308 -               and bo_fg: "bounded {x. ~ (f x = x \<and> g x = x)}"
  20.309 +               and fg_sub: "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S"
  20.310 +               and bo_fg: "bounded {x. \<not> (f x = x \<and> g x = x)}"
  20.311      using insert.IH [OF xyS pw] insert.prems by (blast intro: that)
  20.312    then have "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(x i) = y i) \<and>
  20.313 -                   {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
  20.314 +                   {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
  20.315      using insert by blast
  20.316    have aff_eq: "affine hull (S - y ` K) = affine hull S"
  20.317      apply (rule affine_hull_Diff)
  20.318 @@ -7832,7 +7832,7 @@
  20.319        using feq hk_sub by (auto simp: heq)
  20.320      show "{x. \<not> ((h \<circ> f) x = x \<and> (g \<circ> k) x = x)} \<subseteq> S"
  20.321        using fg_sub hk_sub by force
  20.322 -    have "bounded ({x. ~(f x = x \<and> g x = x)} \<union> {x. ~(h x = x \<and> k x = x)})"
  20.323 +    have "bounded ({x. \<not>(f x = x \<and> g x = x)} \<union> {x. \<not>(h x = x \<and> k x = x)})"
  20.324        using bo_fg bo_hk bounded_Un by blast
  20.325      then show "bounded {x. \<not> ((h \<circ> f) x = x \<and> (g \<circ> k) x = x)}"
  20.326        by (rule bounded_subset) auto
  20.327 @@ -7846,7 +7846,7 @@
  20.328        and pw: "pairwise (\<lambda>i j. (x i \<noteq> x j) \<and> (y i \<noteq> y j)) K"
  20.329        and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
  20.330    obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
  20.331 -                    "{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
  20.332 +                    "{x. \<not> (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (\<not> (f x = x \<and> g x = x))}"
  20.333  proof (cases "S = {}")
  20.334    case True
  20.335    then show ?thesis
  20.336 @@ -7995,8 +7995,8 @@
  20.337    fixes T :: "real set"
  20.338    assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
  20.339    obtains f g where "homeomorphism T T f g"
  20.340 -                    "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
  20.341 -                    "bounded {x. (~ (f x = x \<and> g x = x))}"
  20.342 +                    "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
  20.343 +                    "bounded {x. (\<not> (f x = x \<and> g x = x))}"
  20.344  proof -
  20.345    obtain c d where "box c d \<noteq> {}" "cbox c d \<subseteq> U"
  20.346    proof -
  20.347 @@ -8109,8 +8109,8 @@
  20.348  proposition homeomorphism_grouping_points_exists:
  20.349    fixes S :: "'a::euclidean_space set"
  20.350    assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
  20.351 -  obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
  20.352 -                    "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
  20.353 +  obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
  20.354 +                    "bounded {x. (\<not> (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
  20.355  proof (cases "2 \<le> DIM('a)")
  20.356    case True
  20.357    have TS: "T \<subseteq> affine hull S"
  20.358 @@ -8172,10 +8172,10 @@
  20.359        using sub hj
  20.360        apply (drule_tac c="h x" in subsetD, force)
  20.361        by (metis imageE)
  20.362 -    have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
  20.363 +    have "bounded (j ` {x. (\<not> (f x = x \<and> g x = x))})"
  20.364        by (rule bounded_linear_image [OF bou]) (use \<open>linear j\<close> linear_conv_bounded_linear in auto)
  20.365      moreover
  20.366 -    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))}"
  20.367 +    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))}"
  20.368        using hj by (auto simp: jf jg image_iff, metis+)
  20.369      ultimately show "bounded {x. \<not> ((j \<circ> f \<circ> h) x = x \<and> (j \<circ> g \<circ> h) x = x)}"
  20.370        by metis
  20.371 @@ -8190,8 +8190,8 @@
  20.372    assumes opeU: "openin (subtopology euclidean S) U"
  20.373        and opeS: "openin (subtopology euclidean (affine hull S)) S"
  20.374        and "U \<noteq> {}" "finite K" "K \<subseteq> S" and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
  20.375 -  obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \<and> g x = x))} \<subseteq> S"
  20.376 -                    "bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
  20.377 +  obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
  20.378 +                    "bounded {x. (\<not> (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
  20.379  proof (cases "2 \<le> aff_dim S")
  20.380    case True
  20.381    have opeU': "openin (subtopology euclidean (affine hull S)) U"
  20.382 @@ -8208,7 +8208,7 @@
  20.383    then obtain \<gamma> where \<gamma>: "bij_betw \<gamma> K P"
  20.384      using \<open>finite K\<close> finite_same_card_bij by blast
  20.385    have "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(id i) = \<gamma> i) \<and>
  20.386 -               {x. ~ (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. ~ (f x = x \<and> g x = x)}"
  20.387 +               {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
  20.388    proof (rule homeomorphism_moving_points_exists_gen [OF \<open>finite K\<close> _ _ True opeS S])
  20.389      show "\<And>i. i \<in> K \<Longrightarrow> id i \<in> S \<and> \<gamma> i \<in> S"
  20.390        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)
  20.391 @@ -8314,10 +8314,10 @@
  20.392      next
  20.393        have "compact (j ` closure {x. \<not> (f x = x \<and> g x = x)})"
  20.394          using bou by (auto simp: compact_continuous_image cont_hj)
  20.395 -      then have "bounded (j ` {x. (~ (f x = x \<and> g x = x))})"
  20.396 +      then have "bounded (j ` {x. \<not> (f x = x \<and> g x = x)})"
  20.397          by (rule bounded_closure_image [OF compact_imp_bounded])
  20.398        moreover
  20.399 -      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))}"
  20.400 +      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))}"
  20.401          using h j by (auto simp: image_iff; metis)
  20.402        ultimately have "bounded {x \<in> affine hull S. j (f (h x)) \<noteq> x \<or> j (g (h x)) \<noteq> x}"
  20.403          by metis
  20.404 @@ -8337,7 +8337,7 @@
  20.405    qed
  20.406  qed
  20.407  
  20.408 -subsection\<open>nullhomotopic mappings\<close>
  20.409 +subsection\<open>Nullhomotopic mappings\<close>
  20.410  
  20.411  text\<open> A mapping out of a sphere is nullhomotopic iff it extends to the ball.
  20.412  This even works out in the degenerate cases when the radius is \<open>\<le>\<close> 0, and
    21.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Wed Dec 26 20:57:23 2018 +0100
    21.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Thu Dec 27 19:48:28 2018 +0100
    21.3 @@ -169,7 +169,7 @@
    21.4       by auto
    21.5     have c0: "c 0 = - (a * b 0)" using  b [of 0]
    21.6       by simp
    21.7 -   then have extr_prem: "~ (\<exists>k\<le>n. b k \<noteq> 0) \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> k \<le> Suc n \<and> c k \<noteq> 0"
    21.8 +   then have extr_prem: "\<not> (\<exists>k\<le>n. b k \<noteq> 0) \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> k \<le> Suc n \<and> c k \<noteq> 0"
    21.9       by (metis Suc.prems le0 minus_zero mult_zero_right)
   21.10     have "\<exists>k\<le>n. b k \<noteq> 0"
   21.11       apply (rule ccontr)
   21.12 @@ -205,7 +205,7 @@
   21.13      shows  "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0) \<longleftrightarrow> (\<forall>k. k \<le> n \<longrightarrow> c k = 0)"
   21.14  proof (cases "(\<forall>z. (\<Sum>i\<le>n. c i * z^i) = 0)")
   21.15    case True
   21.16 -  then have "~ finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
   21.17 +  then have "\<not> finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
   21.18      by (simp add: infinite_UNIV_char_0)
   21.19    with True show ?thesis
   21.20      by (metis (poly_guards_query) polyfun_rootbound_finite)
    22.1 --- a/src/HOL/Analysis/Polytope.thy	Wed Dec 26 20:57:23 2018 +0100
    22.2 +++ b/src/HOL/Analysis/Polytope.thy	Thu Dec 27 19:48:28 2018 +0100
    22.3 @@ -270,7 +270,7 @@
    22.4  
    22.5  lemma%unimportant subset_of_face_of_affine_hull:
    22.6      fixes S :: "'a::euclidean_space set"
    22.7 -  assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "~disjnt (affine hull T) (rel_interior U)"
    22.8 +  assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "\<not> disjnt (affine hull T) (rel_interior U)"
    22.9    shows "U \<subseteq> T"
   22.10    apply (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
   22.11    using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T]
   22.12 @@ -846,10 +846,10 @@
   22.13        using affine_parallel_slice affine_affine_hull by metis 
   22.14      show ?thesis
   22.15      proof (intro conjI impI allI ballI exI)
   22.16 -      have *: "S \<subseteq> - (affine hull S \<inter> {x. P x}) \<union> affine hull S \<inter> {x. Q x} \<Longrightarrow> S \<subseteq> {x. ~P x \<or> Q x}" 
   22.17 +      have *: "S \<subseteq> - (affine hull S \<inter> {x. P x}) \<union> affine hull S \<inter> {x. Q x} \<Longrightarrow> S \<subseteq> {x. \<not> P x \<or> Q x}" 
   22.18          for P Q 
   22.19          using hull_subset by fastforce  
   22.20 -      have "S \<subseteq> {x. ~ (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
   22.21 +      have "S \<subseteq> {x. \<not> (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
   22.22          apply (rule *)
   22.23          apply (simp only: le eq)
   22.24          using Ssub by auto
   22.25 @@ -919,7 +919,7 @@
   22.26     "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
   22.27  using%unimportant extreme_point_of_convex_hull by auto
   22.28  
   22.29 -lemma%unimportant extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
   22.30 +lemma%unimportant extreme_point_of_empty [simp]: "\<not> (x extreme_point_of {})"
   22.31    by (simp add: extreme_point_of_def)
   22.32  
   22.33  lemma%unimportant extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   22.34 @@ -974,10 +974,10 @@
   22.35                      (infixr "(facet'_of)" 50)
   22.36    where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
   22.37  
   22.38 -lemma%unimportant facet_of_empty [simp]: "~ S facet_of {}"
   22.39 +lemma%unimportant facet_of_empty [simp]: "\<not> S facet_of {}"
   22.40    by (simp add: facet_of_def)
   22.41  
   22.42 -lemma%unimportant facet_of_irrefl [simp]: "~ S facet_of S "
   22.43 +lemma%unimportant facet_of_irrefl [simp]: "\<not> S facet_of S "
   22.44    by (simp add: facet_of_def)
   22.45  
   22.46  lemma%unimportant facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   22.47 @@ -1088,7 +1088,7 @@
   22.48        using * [of "norm b" "norm a" "1-u" for u] noax that
   22.49          apply (simp add: add.commute)
   22.50        done
   22.51 -    ultimately have "~ (norm a < norm x) \<and> ~ (norm b < norm x)"
   22.52 +    ultimately have "\<not> (norm a < norm x) \<and> \<not> (norm b < norm x)"
   22.53        by auto
   22.54      then show ?thesis
   22.55        using different_norm_3_collinear_points noax nobx that(3) by fastforce
   22.56 @@ -1268,7 +1268,7 @@
   22.57  lemma%unimportant extreme_point_of_convex_hull_affine_independent:
   22.58    fixes S :: "'a::euclidean_space set"
   22.59    shows
   22.60 -   "~ affine_dependent S
   22.61 +   "\<not> affine_dependent S
   22.62           \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
   22.63  by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
   22.64  
   22.65 @@ -1473,7 +1473,7 @@
   22.66  
   22.67  proposition%important face_of_convex_hull_affine_independent:
   22.68    fixes S :: "'a::euclidean_space set"
   22.69 -  assumes "~ affine_dependent S"
   22.70 +  assumes "\<not> affine_dependent S"
   22.71      shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
   22.72            (is "?lhs = ?rhs")
   22.73  proof%unimportant
   22.74 @@ -1495,7 +1495,7 @@
   22.75  
   22.76  lemma%unimportant facet_of_convex_hull_affine_independent:
   22.77    fixes S :: "'a::euclidean_space set"
   22.78 -  assumes "~ affine_dependent S"
   22.79 +  assumes "\<not> affine_dependent S"
   22.80      shows "T facet_of (convex hull S) \<longleftrightarrow>
   22.81             T \<noteq> {} \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u}))"
   22.82            (is "?lhs = ?rhs")
   22.83 @@ -1508,7 +1508,7 @@
   22.84      by (auto simp: face_of_convex_hull_affine_independent [OF assms])
   22.85    then have affs: "aff_dim S = aff_dim c + 1"
   22.86      by (metis aff_dim_convex_hull afft eq_diff_eq)
   22.87 -  have "~ affine_dependent c"
   22.88 +  have "\<not> affine_dependent c"
   22.89      using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
   22.90    with affs have "card (S - c) = 1"
   22.91      apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
   22.92 @@ -1543,7 +1543,7 @@
   22.93  lemma%unimportant facet_of_convex_hull_affine_independent_alt:
   22.94    fixes S :: "'a::euclidean_space set"
   22.95    shows
   22.96 -   "~affine_dependent S
   22.97 +   "\<not>affine_dependent S
   22.98          \<Longrightarrow> (T facet_of (convex hull S) \<longleftrightarrow>
   22.99               2 \<le> card S \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u})))"
  22.100  apply (simp add: facet_of_convex_hull_affine_independent)
  22.101 @@ -1897,20 +1897,20 @@
  22.102      have "\<exists>a' b'. a' \<noteq> 0 \<and>
  22.103                    affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> h \<and>
  22.104                    (\<forall>w \<in> affine hull S. (w + a') \<in> affine hull S)"
  22.105 -        if "h \<in> F" "~(affine hull S \<subseteq> h)" for h
  22.106 +        if "h \<in> F" "\<not>(affine hull S \<subseteq> h)" for h
  22.107      proof -
  22.108        have "a h \<noteq> 0" and "h = {x. a h \<bullet> x \<le> b h}" "h \<inter> \<Inter>F = \<Inter>F"
  22.109          using \<open>h \<in> F\<close> ab by auto
  22.110        then have "(affine hull S) \<inter> {x. a h \<bullet> x \<le> b h} \<noteq> {}"
  22.111          by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2))
  22.112 -      moreover have "~ (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
  22.113 +      moreover have "\<not> (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
  22.114          using \<open>h = {x. a h \<bullet> x \<le> b h}\<close> that(2) by blast
  22.115        ultimately show ?thesis
  22.116          using affine_parallel_slice [of "affine hull S"]
  22.117          by (metis \<open>h = {x. a h \<bullet> x \<le> b h}\<close> affine_affine_hull)
  22.118      qed
  22.119      then obtain a b
  22.120 -         where ab: "\<And>h. \<lbrakk>h \<in> F; ~ (affine hull S \<subseteq> h)\<rbrakk>
  22.121 +         where ab: "\<And>h. \<lbrakk>h \<in> F; \<not> (affine hull S \<subseteq> h)\<rbrakk>
  22.122               \<Longrightarrow> a h \<noteq> 0 \<and>
  22.123                    affine hull S \<inter> {x. a h \<bullet> x \<le> b h} = affine hull S \<inter> h \<and>
  22.124                    (\<forall>w \<in> affine hull S. (w + a h) \<in> affine hull S)"
  22.125 @@ -1918,7 +1918,7 @@
  22.126      have seq2: "S = affine hull S \<inter> (\<Inter>h\<in>{h \<in> F. \<not> affine hull S \<subseteq> h}. {x. a h \<bullet> x \<le> b h})"
  22.127        by (subst seq) (auto simp: ab INT_extend_simps)
  22.128      show ?thesis
  22.129 -      apply (rule_tac x="(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h. h \<in> F \<and> ~(affine hull S \<subseteq> h)}" in exI)
  22.130 +      apply (rule_tac x="(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h. h \<in> F \<and> \<not>(affine hull S \<subseteq> h)}" in exI)
  22.131        apply (intro conjI seq2)
  22.132          using \<open>finite F\<close> apply force
  22.133         using ab apply blast
  22.134 @@ -1958,9 +1958,9 @@
  22.135      done
  22.136    then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F"
  22.137      by blast
  22.138 -  then have "~ (finite g \<and> ?P g \<and> ?Q g)" if "card g < n" for g
  22.139 +  then have "\<not> (finite g \<and> ?P g \<and> ?Q g)" if "card g < n" for g
  22.140      using that by (auto simp: n_def dest!: not_less_Least)
  22.141 -  then have *: "~ (?P g \<and> ?Q g)" if "g \<subset> F" for g
  22.142 +  then have *: "\<not> (?P g \<and> ?Q g)" if "g \<subset> F" for g
  22.143      using that \<open>finite F\<close> psubset_card_mono \<open>card F = n\<close>
  22.144      by (metis finite_Int inf.strict_order_iff)
  22.145    have 1: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subseteq> affine hull S \<inter> \<Inter>F'"
  22.146 @@ -2230,7 +2230,7 @@
  22.147      using seq by blast
  22.148    have "F \<noteq> {}" using assms
  22.149      by (metis affine_Int affine_Inter affine_affine_hull ex_in_conv face_of_affine_trivial)
  22.150 -  then obtain i where "i \<in> F" "~ (a i \<bullet> x < b i)"
  22.151 +  then obtain i where "i \<in> F" "\<not> (a i \<bullet> x < b i)"
  22.152      using \<open>x \<in> S\<close> rels xnot by auto
  22.153    with xint have "a i \<bullet> x = b i"
  22.154      by (metis eq_iff mem_Collect_eq not_le Inter_iff faceq)
  22.155 @@ -2745,7 +2745,7 @@
  22.156  
  22.157  lemma rel_boundary_of_convex_hull:
  22.158      fixes S :: "'a::euclidean_space set"
  22.159 -    assumes "~ affine_dependent S"
  22.160 +    assumes "\<not> affine_dependent S"
  22.161        shows "(convex hull S) - rel_interior(convex hull S) = (\<Union>a\<in>S. convex hull (S - {a}))"
  22.162  proof -
  22.163    have "finite S" by (metis assms aff_independent_finite)
  22.164 @@ -3074,17 +3074,17 @@
  22.165  
  22.166  text\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
  22.167  definition simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
  22.168 -  where "n simplex S \<equiv> \<exists>C. ~(affine_dependent C) \<and> int(card C) = n + 1 \<and> S = convex hull C"
  22.169 +  where "n simplex S \<equiv> \<exists>C. \<not> affine_dependent C \<and> int(card C) = n + 1 \<and> S = convex hull C"
  22.170  
  22.171  lemma simplex:
  22.172      "n simplex S \<longleftrightarrow> (\<exists>C. finite C \<and>
  22.173 -                       ~(affine_dependent C) \<and>
  22.174 +                       \<not> affine_dependent C \<and>
  22.175                         int(card C) = n + 1 \<and>
  22.176                         S = convex hull C)"
  22.177    by (auto simp add: simplex_def intro: aff_independent_finite)
  22.178  
  22.179  lemma simplex_convex_hull:
  22.180 -   "~affine_dependent C \<and> int(card C) = n + 1 \<Longrightarrow> n simplex (convex hull C)"
  22.181 +   "\<not> affine_dependent C \<and> int(card C) = n + 1 \<Longrightarrow> n simplex (convex hull C)"
  22.182    by (auto simp add: simplex_def)
  22.183  
  22.184  lemma convex_simplex: "n simplex S \<Longrightarrow> convex S"
  22.185 @@ -3170,7 +3170,7 @@
  22.186    assumes "n simplex S" and a: "a \<notin> affine hull S"
  22.187    shows "(n+1) simplex (convex hull (insert a S))"
  22.188  proof -
  22.189 -  obtain C where C: "finite C" "~(affine_dependent C)" "int(card C) = n+1" and S: "S = convex hull C"
  22.190 +  obtain C where C: "finite C" "\<not> affine_dependent C" "int(card C) = n+1" and S: "S = convex hull C"
  22.191      using assms unfolding simplex by force
  22.192    show ?thesis
  22.193      unfolding simplex
  22.194 @@ -3270,11 +3270,11 @@
  22.195                U [unfolded rel_frontier_def] tnot
  22.196              by (auto simp: closed_segment_eq_open)
  22.197            ultimately
  22.198 -          have "~(between (t,u) z | between (u,z) t | between (z,t) u)" if "x \<noteq> z"
  22.199 +          have "\<not>(between (t,u) z | between (u,z) t | between (z,t) u)" if "x \<noteq> z"
  22.200              using that xt xu
  22.201              apply (simp add: between_mem_segment [symmetric])
  22.202              by (metis between_commute between_trans_2 between_antisym)
  22.203 -          then have "~ collinear {t, z, u}" if "x \<noteq> z"
  22.204 +          then have "\<not> collinear {t, z, u}" if "x \<noteq> z"
  22.205              by (auto simp: that collinear_between_cases between_commute)
  22.206            moreover have "collinear {t, z, x}"
  22.207              by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xt)
  22.208 @@ -3352,7 +3352,7 @@
  22.209        by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
  22.210      have in_rel_interior: "(SOME z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
  22.211          using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
  22.212 -    have *: "\<exists>T. ~affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
  22.213 +    have *: "\<exists>T. \<not> affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
  22.214        if "K \<in> \<U>" for K
  22.215      proof -
  22.216        obtain r where r: "r simplex K"
    23.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Wed Dec 26 20:57:23 2018 +0100
    23.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Thu Dec 27 19:48:28 2018 +0100
    23.3 @@ -860,7 +860,7 @@
    23.4  lemma frontier_properties:
    23.5    assumes "simply_connected S"
    23.6    shows "if bounded S then connected(frontier S)
    23.7 -         else \<forall>C \<in> components(frontier S). ~bounded C"
    23.8 +         else \<forall>C \<in> components(frontier S). \<not> bounded C"
    23.9  proof -
   23.10    have "S = {} \<or> S homeomorphic ball (0::complex) 1"
   23.11      using simply_connected_eq_homeomorphic_to_disc assms openS by blast
   23.12 @@ -1217,7 +1217,7 @@
   23.13  qed
   23.14  
   23.15  lemma empty_inside:
   23.16 -  assumes "connected S" "\<And>C. C \<in> components (- S) \<Longrightarrow> ~bounded C"
   23.17 +  assumes "connected S" "\<And>C. C \<in> components (- S) \<Longrightarrow> \<not> bounded C"
   23.18    shows "inside S = {}"
   23.19    using assms by (auto simp: components_def inside_def)
   23.20  
    24.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Dec 26 20:57:23 2018 +0100
    24.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Dec 27 19:48:28 2018 +0100
    24.3 @@ -3726,7 +3726,7 @@
    24.4  
    24.5  lemma affine_independent_convex_affine_hull:
    24.6    fixes s :: "'a::euclidean_space set"
    24.7 -  assumes "~affine_dependent s" "t \<subseteq> s"
    24.8 +  assumes "\<not> affine_dependent s" "t \<subseteq> s"
    24.9      shows "convex hull t = affine hull t \<inter> convex hull s"
   24.10  proof -
   24.11    have fin: "finite s" "finite t" using assms aff_independent_finite finite_subset by auto
   24.12 @@ -3764,7 +3764,7 @@
   24.13  
   24.14  lemma affine_independent_span_eq:
   24.15    fixes s :: "'a::euclidean_space set"
   24.16 -  assumes "~affine_dependent s" "card s = Suc (DIM ('a))"
   24.17 +  assumes "\<not> affine_dependent s" "card s = Suc (DIM ('a))"
   24.18      shows "affine hull s = UNIV"
   24.19  proof (cases "s = {}")
   24.20    case True then show ?thesis
   24.21 @@ -3789,7 +3789,7 @@
   24.22  
   24.23  lemma affine_independent_span_gt:
   24.24    fixes s :: "'a::euclidean_space set"
   24.25 -  assumes ind: "~ affine_dependent s" and dim: "DIM ('a) < card s"
   24.26 +  assumes ind: "\<not> affine_dependent s" and dim: "DIM ('a) < card s"
   24.27      shows "affine hull s = UNIV"
   24.28    apply (rule affine_independent_span_eq [OF ind])
   24.29    apply (rule antisym)
   24.30 @@ -3831,7 +3831,7 @@
   24.31  
   24.32  lemma rel_interior_convex_hull_explicit:
   24.33    fixes s :: "'a::euclidean_space set"
   24.34 -  assumes "~ affine_dependent s"
   24.35 +  assumes "\<not> affine_dependent s"
   24.36    shows "rel_interior(convex hull s) =
   24.37           {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
   24.38           (is "?lhs = ?rhs")
   24.39 @@ -3904,18 +3904,18 @@
   24.40  lemma interior_convex_hull_explicit_minimal:
   24.41    fixes s :: "'a::euclidean_space set"
   24.42    shows
   24.43 -   "~ affine_dependent s
   24.44 +   "\<not> affine_dependent s
   24.45          ==> interior(convex hull s) =
   24.46               (if card(s) \<le> DIM('a) then {}
   24.47                else {y. \<exists>u. (\<forall>x \<in> s. 0 < u x) \<and> sum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = y})"
   24.48    apply (simp add: aff_independent_finite empty_interior_convex_hull, clarify)
   24.49    apply (rule trans [of _ "rel_interior(convex hull s)"])
   24.50 -  apply (simp add: affine_hull_convex_hull affine_independent_span_gt rel_interior_interior)
   24.51 +  apply (simp add: affine_independent_span_gt rel_interior_interior)
   24.52    by (simp add: rel_interior_convex_hull_explicit)
   24.53  
   24.54  lemma interior_convex_hull_explicit:
   24.55    fixes s :: "'a::euclidean_space set"
   24.56 -  assumes "~ affine_dependent s"
   24.57 +  assumes "\<not> affine_dependent s"
   24.58    shows
   24.59     "interior(convex hull s) =
   24.60               (if card(s) \<le> DIM('a) then {}
   24.61 @@ -4082,7 +4082,7 @@
   24.62  
   24.63  lemma rel_frontier_convex_hull_explicit:
   24.64    fixes s :: "'a::euclidean_space set"
   24.65 -  assumes "~ affine_dependent s"
   24.66 +  assumes "\<not> affine_dependent s"
   24.67    shows "rel_frontier(convex hull s) =
   24.68           {y. \<exists>u. (\<forall>x \<in> s. 0 \<le> u x) \<and> (\<exists>x \<in> s. u x = 0) \<and> sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
   24.69  proof -
   24.70 @@ -4106,7 +4106,7 @@
   24.71  
   24.72  lemma frontier_convex_hull_explicit:
   24.73    fixes s :: "'a::euclidean_space set"
   24.74 -  assumes "~ affine_dependent s"
   24.75 +  assumes "\<not> affine_dependent s"
   24.76    shows "frontier(convex hull s) =
   24.77           {y. \<exists>u. (\<forall>x \<in> s. 0 \<le> u x) \<and> (DIM ('a) < card s \<longrightarrow> (\<exists>x \<in> s. u x = 0)) \<and>
   24.78               sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
   24.79 @@ -4133,7 +4133,7 @@
   24.80  
   24.81  lemma rel_frontier_convex_hull_cases:
   24.82    fixes s :: "'a::euclidean_space set"
   24.83 -  assumes "~ affine_dependent s"
   24.84 +  assumes "\<not> affine_dependent s"
   24.85    shows "rel_frontier(convex hull s) = \<Union>{convex hull (s - {x}) |x. x \<in> s}"
   24.86  proof -
   24.87    have fs: "finite s"
   24.88 @@ -4164,7 +4164,7 @@
   24.89  
   24.90  lemma frontier_convex_hull_eq_rel_frontier:
   24.91    fixes s :: "'a::euclidean_space set"
   24.92 -  assumes "~ affine_dependent s"
   24.93 +  assumes "\<not> affine_dependent s"
   24.94    shows "frontier(convex hull s) =
   24.95             (if card s \<le> DIM ('a) then convex hull s else rel_frontier(convex hull s))"
   24.96    using assms
   24.97 @@ -4174,7 +4174,7 @@
   24.98  
   24.99  lemma frontier_convex_hull_cases:
  24.100    fixes s :: "'a::euclidean_space set"
  24.101 -  assumes "~ affine_dependent s"
  24.102 +  assumes "\<not> affine_dependent s"
  24.103    shows "frontier(convex hull s) =
  24.104             (if card s \<le> DIM ('a) then convex hull s else \<Union>{convex hull (s - {x}) |x. x \<in> s})"
  24.105  by (simp add: assms frontier_convex_hull_eq_rel_frontier rel_frontier_convex_hull_cases)
  24.106 @@ -4668,7 +4668,7 @@
  24.107  
  24.108  lemma interior_convex_hull_3_minimal:
  24.109    fixes a :: "'a::euclidean_space"
  24.110 -  shows "\<lbrakk>~ collinear{a,b,c}; DIM('a) = 2\<rbrakk>
  24.111 +  shows "\<lbrakk>\<not> collinear{a,b,c}; DIM('a) = 2\<rbrakk>
  24.112           \<Longrightarrow> interior(convex hull {a,b,c}) =
  24.113                  {v. \<exists>x y z. 0 < x \<and> 0 < y \<and> 0 < z \<and> x + y + z = 1 \<and>
  24.114                              x *\<^sub>R a + y *\<^sub>R b + z *\<^sub>R c = v}"
  24.115 @@ -5862,7 +5862,7 @@
  24.116  
  24.117  lemma affine_dependent_choose:
  24.118    fixes a :: "'a :: euclidean_space"
  24.119 -  assumes "~(affine_dependent S)"
  24.120 +  assumes "\<not>(affine_dependent S)"
  24.121    shows "affine_dependent(insert a S) \<longleftrightarrow> a \<notin> S \<and> a \<in> affine hull S"
  24.122          (is "?lhs = ?rhs")
  24.123  proof safe
  24.124 @@ -5887,7 +5887,7 @@
  24.125  
  24.126  lemma affine_independent_insert:
  24.127    fixes a :: "'a :: euclidean_space"
  24.128 -  shows "\<lbrakk>~(affine_dependent S); a \<notin> affine hull S\<rbrakk> \<Longrightarrow> ~(affine_dependent(insert a S))"
  24.129 +  shows "\<lbrakk>\<not> affine_dependent S; a \<notin> affine hull S\<rbrakk> \<Longrightarrow> \<not> affine_dependent(insert a S)"
  24.130    by (simp add: affine_dependent_choose)
  24.131  
  24.132  lemma subspace_bounded_eq_trivial:
  24.133 @@ -6158,7 +6158,7 @@
  24.134  
  24.135  lemma
  24.136    fixes s :: "'a::euclidean_space set"
  24.137 -  assumes "~ (affine_dependent(s \<union> t))"
  24.138 +  assumes "\<not> affine_dependent(s \<union> t)"
  24.139      shows convex_hull_Int_subset: "convex hull s \<inter> convex hull t \<subseteq> convex hull (s \<inter> t)" (is ?C)
  24.140        and affine_hull_Int_subset: "affine hull s \<inter> affine hull t \<subseteq> affine hull (s \<inter> t)" (is ?A)
  24.141  proof -
  24.142 @@ -6201,7 +6201,7 @@
  24.143  
  24.144  proposition affine_hull_Int:
  24.145    fixes s :: "'a::euclidean_space set"
  24.146 -  assumes "~ (affine_dependent(s \<union> t))"
  24.147 +  assumes "\<not> affine_dependent(s \<union> t)"
  24.148      shows "affine hull (s \<inter> t) = affine hull s \<inter> affine hull t"
  24.149  apply (rule subset_antisym)
  24.150  apply (simp add: hull_mono)
  24.151 @@ -6209,7 +6209,7 @@
  24.152  
  24.153  proposition convex_hull_Int:
  24.154    fixes s :: "'a::euclidean_space set"
  24.155 -  assumes "~ (affine_dependent(s \<union> t))"
  24.156 +  assumes "\<not> affine_dependent(s \<union> t)"
  24.157      shows "convex hull (s \<inter> t) = convex hull s \<inter> convex hull t"
  24.158  apply (rule subset_antisym)
  24.159  apply (simp add: hull_mono)
  24.160 @@ -6217,7 +6217,7 @@
  24.161  
  24.162  proposition
  24.163    fixes s :: "'a::euclidean_space set set"
  24.164 -  assumes "~ (affine_dependent (\<Union>s))"
  24.165 +  assumes "\<not> affine_dependent (\<Union>s)"
  24.166      shows affine_hull_Inter: "affine hull (\<Inter>s) = (\<Inter>t\<in>s. affine hull t)" (is "?A")
  24.167        and convex_hull_Inter: "convex hull (\<Inter>s) = (\<Inter>t\<in>s. convex hull t)" (is "?C")
  24.168  proof -
  24.169 @@ -6247,7 +6247,7 @@
  24.170  
  24.171  proposition in_convex_hull_exchange_unique:
  24.172    fixes S :: "'a::euclidean_space set"
  24.173 -  assumes naff: "~ affine_dependent S" and a: "a \<in> convex hull S"
  24.174 +  assumes naff: "\<not> affine_dependent S" and a: "a \<in> convex hull S"
  24.175        and S: "T \<subseteq> S" "T' \<subseteq> S"
  24.176        and x:  "x \<in> convex hull (insert a T)"
  24.177        and x': "x \<in> convex hull (insert a T')"
  24.178 @@ -6395,7 +6395,7 @@
  24.179  
  24.180  corollary convex_hull_exchange_Int:
  24.181    fixes a  :: "'a::euclidean_space"
  24.182 -  assumes "~ affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
  24.183 +  assumes "\<not> affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
  24.184    shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
  24.185           convex hull (insert a (T \<inter> T'))"
  24.186  apply (rule subset_antisym)
  24.187 @@ -6404,7 +6404,7 @@
  24.188  
  24.189  lemma Int_closed_segment:
  24.190    fixes b :: "'a::euclidean_space"
  24.191 -  assumes "b \<in> closed_segment a c \<or> ~collinear{a,b,c}"
  24.192 +  assumes "b \<in> closed_segment a c \<or> \<not> collinear{a,b,c}"
  24.193      shows "closed_segment a b \<inter> closed_segment b c = {b}"
  24.194  proof (cases "c = a")
  24.195    case True
  24.196 @@ -7283,7 +7283,7 @@
  24.197    fixes S :: "'a :: euclidean_space set"
  24.198    assumes "affine S"
  24.199        and "S \<inter> {x. a \<bullet> x \<le> b} \<noteq> {}"
  24.200 -      and "~ (S \<subseteq> {x. a \<bullet> x \<le> b})"
  24.201 +      and "\<not> (S \<subseteq> {x. a \<bullet> x \<le> b})"
  24.202    obtains a' b' where "a' \<noteq> 0"
  24.203                     "S \<inter> {x. a' \<bullet> x \<le> b'} = S \<inter> {x. a \<bullet> x \<le> b}"
  24.204                     "S \<inter> {x. a' \<bullet> x = b'} = S \<inter> {x. a \<bullet> x = b}"
  24.205 @@ -7669,7 +7669,7 @@
  24.206    assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
  24.207        and opT: "openin (subtopology euclidean (S \<union> T)) T"
  24.208        and contf: "continuous_on S f" and contg: "continuous_on T g"
  24.209 -      and fg: "\<And>x. x \<in> S \<and> ~P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
  24.210 +      and fg: "\<And>x. x \<in> S \<and> \<not>P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
  24.211      shows "continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
  24.212  proof -
  24.213    have "\<And>x. x \<in> S \<Longrightarrow> (if P x then f x else g x) = f x"  "\<And>x. x \<in> T \<Longrightarrow> (if P x then f x else g x) = g x"
    25.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Wed Dec 26 20:57:23 2018 +0100
    25.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Dec 27 19:48:28 2018 +0100
    25.3 @@ -1360,7 +1360,7 @@
    25.4      and k: "k \<in> Basis"
    25.5    shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l . l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subseteq>
    25.6        division_points (cbox a b) d" (is ?t1)
    25.7 -    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
    25.8 +    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> \<not>(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
    25.9        division_points (cbox a b) d" (is ?t2)
   25.10  proof%unimportant -
   25.11    note assm = division_ofD[OF assms(1)]
   25.12 @@ -2536,7 +2536,7 @@
   25.13      show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
   25.14        using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
   25.15    qed
   25.16 -  let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
   25.17 +  let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> \<not>(K \<subseteq> K')}"
   25.18    show ?thesis
   25.19    proof (rule that)
   25.20      show "countable ?\<D>"
    26.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
    26.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
    26.3 @@ -1104,7 +1104,7 @@
    26.4  
    26.5  lemma connected_openin:
    26.6        "connected S \<longleftrightarrow>
    26.7 -       ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
    26.8 +       \<not>(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
    26.9                   openin (subtopology euclidean S) E2 \<and>
   26.10                   S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   26.11    apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
   26.12 @@ -1113,7 +1113,7 @@
   26.13  
   26.14  lemma connected_openin_eq:
   26.15        "connected S \<longleftrightarrow>
   26.16 -       ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
   26.17 +       \<not>(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
   26.18                   openin (subtopology euclidean S) E2 \<and>
   26.19                   E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   26.20                   E1 \<noteq> {} \<and> E2 \<noteq> {})"
   26.21 @@ -1152,7 +1152,7 @@
   26.22  
   26.23  lemma connected_closedin_eq:
   26.24        "connected S \<longleftrightarrow>
   26.25 -           ~(\<exists>E1 E2.
   26.26 +           \<not>(\<exists>E1 E2.
   26.27                   closedin (subtopology euclidean S) E1 \<and>
   26.28                   closedin (subtopology euclidean S) E2 \<and>
   26.29                   E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   26.30 @@ -1946,7 +1946,7 @@
   26.31      by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
   26.32  qed
   26.33  
   26.34 -subsection \<open>Intervals in general, including infinite and mixtures of open and closed\<close>
   26.35 +subsection \<open>General Intervals\<close>
   26.36  
   26.37  definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   26.38    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   26.39 @@ -3645,7 +3645,7 @@
   26.40  
   26.41  corollary cobounded_imp_unbounded:
   26.42      fixes S :: "'a::{real_normed_vector, perfect_space} set"
   26.43 -    shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
   26.44 +    shows "bounded (- S) \<Longrightarrow> \<not> bounded S"
   26.45    using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
   26.46  
   26.47  lemma bounded_dist_comp:
   26.48 @@ -4743,7 +4743,7 @@
   26.49  
   26.50  lemma not_compact_UNIV[simp]:
   26.51    fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set"
   26.52 -  shows "~ compact (UNIV::'a set)"
   26.53 +  shows "\<not> compact (UNIV::'a set)"
   26.54      by (simp add: compact_eq_bounded_closed)
   26.55  
   26.56  text\<open>Representing sets as the union of a chain of compact sets.\<close>
    27.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Dec 26 20:57:23 2018 +0100
    27.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Dec 27 19:48:28 2018 +0100
    27.3 @@ -767,7 +767,7 @@
    27.4    assumes "compact S"  "\<And>c. P(\<lambda>x. c::real)"
    27.5            "\<And>f. P f \<Longrightarrow> continuous_on S f"
    27.6            "\<And>f g. P(f) \<and> P(g) \<Longrightarrow> P(\<lambda>x. f x + g x)"  "\<And>f g. P(f) \<and> P(g) \<Longrightarrow> P(\<lambda>x. f x * g x)"
    27.7 -          "\<And>x y. x \<in> S \<and> y \<in> S \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)"
    27.8 +          "\<And>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y \<Longrightarrow> \<exists>f. P(f) \<and> f x \<noteq> f y"
    27.9            "continuous_on S f"
   27.10         "0 < e"
   27.11      shows "\<exists>g. P(g) \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> < e)"
    28.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Wed Dec 26 20:57:23 2018 +0100
    28.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Thu Dec 27 19:48:28 2018 +0100
    28.3 @@ -22,7 +22,7 @@
    28.4  
    28.5  lemma wn_triangle1:
    28.6    assumes "0 \<in> interior(convex hull {a,b,c})"
    28.7 -    shows "~ (Im(a/b) \<le> 0 \<and> 0 \<le> Im(b/c))"
    28.8 +    shows "\<not> (Im(a/b) \<le> 0 \<and> 0 \<le> Im(b/c))"
    28.9  proof -
   28.10    { assume 0: "Im(a/b) \<le> 0" "0 \<le> Im(b/c)"
   28.11      have "0 \<notin> interior (convex hull {a,b,c})"
   28.12 @@ -224,7 +224,7 @@
   28.13      by (simp_all add: assms path_image_join)
   28.14    with \<open>0 < e\<close> dac have "c \<notin> affine hull {a - of_real e, a + of_real e}"
   28.15      by (simp add: segment_as_ball not_le)
   28.16 -  with \<open>0 < e\<close> have *: "~collinear{a - e, c,a + e}"
   28.17 +  with \<open>0 < e\<close> have *: "\<not> collinear {a - e, c,a + e}"
   28.18      using collinear_3_affine_hull [of "a-e" "a+e"] by (auto simp: insert_commute)
   28.19    have 13: "1/3 + 1/3 + 1/3 = (1::real)" by simp
   28.20    have "(1/3) *\<^sub>R (a - of_real e) + (1/3) *\<^sub>R c + (1/3) *\<^sub>R (a + of_real e) \<in> interior(convex hull {a - e, c, a + e})"