# HG changeset patch
# User wenzelm
# Date 1479582632 -3600
# Node ID 874555896035f15218aeb5a7aa57efedb8fb206f
# Parent  eace715f498830536257e57a9d141732cfc123e2
more symbols;

diff -r eace715f4988 -r 874555896035 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Nov 19 19:43:09 2016 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Nov 19 20:10:32 2016 +0100
@@ -3265,8 +3265,8 @@
 
 lemma homotopic_circlemaps_imp_homotopic_loops:
   assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
-   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
-                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
+   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))
+                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
 proof -
   have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
     using assms by (auto simp: sphere_def)
@@ -3347,7 +3347,7 @@
       and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
     shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
 proof -
-  have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * ii))"
+  have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * \<i>))"
     apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
     apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
     done
diff -r eace715f4988 -r 874555896035 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sat Nov 19 19:43:09 2016 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Sat Nov 19 20:10:32 2016 +0100
@@ -3240,7 +3240,7 @@
     have inj_exp: "inj_on exp (ball (Ln z) 1)"
       apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
       using pi_ge_two by (simp add: ball_subset_ball_iff)
-    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1))"
+    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1))"
     show ?thesis
     proof (intro exI conjI)
       show "z \<in> exp ` (ball(Ln z) 1)"
@@ -3286,7 +3286,7 @@
       proof
         fix u
         assume "u \<in> \<V>"
-        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1)"
+        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1)"
           by (auto simp: \<V>_def)
         have "compact (cball (Ln z) 1)"
           by simp
@@ -3325,7 +3325,7 @@
           apply (force simp:)
           done
         show "\<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
-          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * ii) \<circ> \<gamma>" in exI)
+          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * \<i>) \<circ> \<gamma>" in exI)
           unfolding homeomorphism_def
           apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
              apply (auto simp: \<gamma>exp exp2n cont n)