diff -r 7d59af98af29 -r 2a4c8a2a3f8e src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Dec 27 19:48:28 2018 +0100
@@ -941,7 +941,7 @@
   case True then show ?thesis
     by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath)
 next
-  case False then have "~ f contour_integrable_on (reversepath g)"
+  case False then have "\<not> f contour_integrable_on (reversepath g)"
     by (simp add: assms contour_integrable_reversepath_eq)
   with False show ?thesis by (simp add: not_integrable_contour_integral)
 qed
@@ -5518,7 +5518,7 @@
       and ul_f: "uniform_limit (path_image \<gamma>) f l F"
       and noleB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
       and \<gamma>: "valid_path \<gamma>"
-      and [simp]: "~ (trivial_limit F)"
+      and [simp]: "\<not> trivial_limit F"
   shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
 proof -
   have "0 \<le> B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
@@ -5586,7 +5586,7 @@
 corollary%unimportant contour_integral_uniform_limit_circlepath:
   assumes "\<forall>\<^sub>F n::'a in F. (f n) contour_integrable_on (circlepath z r)"
       and "uniform_limit (sphere z r) f l F"
-      and "~ (trivial_limit F)" "0 < r"
+      and "\<not> trivial_limit F" "0 < r"
     shows "l contour_integrable_on (circlepath z r)"
           "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
   using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
@@ -6550,7 +6550,7 @@
 lemma holomorphic_uniform_limit:
   assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
       and ulim: "uniform_limit (cball z r) f g F"
-      and F:  "~ trivial_limit F"
+      and F:  "\<not> trivial_limit F"
   obtains "continuous_on (cball z r) g" "g holomorphic_on ball z r"
 proof (cases r "0::real" rule: linorder_cases)
   case less then show ?thesis by (force simp: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that)
@@ -6620,7 +6620,7 @@
   assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
                                (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
       and ulim: "uniform_limit (cball z r) f g F"
-      and F:  "~ trivial_limit F" and "0 < r"
+      and F:  "\<not> trivial_limit F" and "0 < r"
   obtains g' where
       "continuous_on (cball z r) g"
       "\<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"