--- 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
--- 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)