src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
 changeset 61070 b72a990adfe2 parent 60809 457abb82fb9e child 61426 d53db136e8fd
```     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:01:21 2015 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:28:08 2015 +0200
1.3 @@ -211,7 +211,7 @@
1.4    by (auto simp: exp_eq abs_mult)
1.5
1.6  lemma exp_integer_2pi:
1.7 -  assumes "n \<in> Ints"
1.8 +  assumes "n \<in> \<int>"
1.9    shows "exp((2 * n * pi) * ii) = 1"
1.10  proof -
1.11    have "exp((2 * n * pi) * ii) = exp 0"
1.12 @@ -751,15 +751,15 @@
1.13      by blast
1.14  qed
1.15
1.16 -lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
1.17 +lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
1.18  proof (cases "z=0")
1.19    case True then show ?thesis
1.20      by simp
1.21  next
1.22    case False
1.23 -  have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
1.24 +  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
1.25      by (metis Arg_eq)
1.26 -  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
1.27 +  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
1.28      using False
1.30    also have "... \<longleftrightarrow> Arg z = 0"
1.31 @@ -955,7 +955,7 @@
1.32  corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
1.34
1.35 -lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
1.36 +lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
1.37    using Ln_of_real by force
1.38
1.39  lemma Ln_1: "ln 1 = (0::complex)"
1.40 @@ -1565,10 +1565,10 @@
1.41    using lim_Ln_over_power [of 1]
1.42    by simp
1.43
1.44 -lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
1.45 +lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
1.46    using Ln_of_real by force
1.47
1.48 -lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
1.49 +lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"