src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

   by simp
 
 lemma content_pos_le [iff]: "0 \<le> content X"
   by simp
 
-corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
+corollary content_nonneg [simp]: "\<not> content (cbox a b) < 0"
   using not_le by blast
 
 lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
   by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)
 

   using assms has_integral_alt[of f y i] by auto
 
 definition integrable_on (infixr "integrable'_on" 46)
   where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
 
-definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
+definition "integral i f = (SOME y. (f has_integral y) i \<or> \<not> f integrable_on i \<and> y=0)"
 
 lemma integrable_integral[intro]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
   unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
 
-lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
+lemma not_integrable_integral: "\<not> f integrable_on i \<Longrightarrow> integral i f = 0"
   unfolding integrable_on_def integral_def by blast
 
 lemma has_integral_integrable[dest]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
   unfolding integrable_on_def by auto
 

   by (rule some_equality) (auto intro: has_integral_unique)
 
 lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
   by blast
 
-lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> ~ f integrable_on k \<and> y=0"
+lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> \<not> f integrable_on k \<and> y=0"
   unfolding integral_def integrable_on_def
   apply (erule subst)
   apply (rule someI_ex)
   by blast
 

   shows "integral S (\<lambda>x. f x * c) = integral S f * c"
 proof (cases "f integrable_on S \<or> c = 0")
   case True then show ?thesis
     by (force intro: has_integral_mult_left)
 next
-  case False then have "~ (\<lambda>x. f x * c) integrable_on S"
+  case False then have "\<not> (\<lambda>x. f x * c) integrable_on S"
     using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ S "inverse c"]
     by (auto simp add: mult.assoc)
   with False show ?thesis by (simp add: not_integrable_integral)
 qed
 

 lemma integral_cmul [simp]: "integral S (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral S f"
 proof (cases "f integrable_on S \<or> c = 0")
   case True with has_integral_cmul integrable_integral show ?thesis
     by fastforce
 next
-  case False then have "~ (\<lambda>x. c *\<^sub>R f x) integrable_on S"
+  case False then have "\<not> (\<lambda>x. c *\<^sub>R f x) integrable_on S"
     using has_integral_cmul [of "(\<lambda>x. c *\<^sub>R f x)" _ S "inverse c"] by auto
   with False show ?thesis by (simp add: not_integrable_integral)
 qed
 
 lemma integral_mult:

 lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
 proof (cases "f integrable_on S")
   case True then show ?thesis
     by (simp add: has_integral_neg integrable_integral integral_unique)
 next
-  case False then have "~ (\<lambda>x. - f x) integrable_on S"
+  case False then have "\<not> (\<lambda>x. - f x) integrable_on S"
     using has_integral_neg [of "(\<lambda>x. - f x)" _ S ] by auto
   with False show ?thesis by (simp add: not_integrable_integral)
 qed
 
 lemma integral_diff: "f integrable_on S \<Longrightarrow> g integrable_on S \<Longrightarrow>