src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
 changeset 63040 eb4ddd18d635 parent 62963 2d5eff9c3baa
```     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Sun Apr 24 21:31:14 2016 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Apr 25 16:09:26 2016 +0200
1.3 @@ -244,7 +244,7 @@
1.4        hence "convergent (\<lambda>n. X n x)"
1.5          by (metis Cauchy_convergent_iff)
1.6      } note convergent_norm1 = this
1.7 -    def y \<equiv> "x /\<^sub>R norm x"
1.8 +    define y where "y = x /\<^sub>R norm x"
1.9      have y: "norm y \<le> 1" and xy: "x = norm x *\<^sub>R y"
1.10        by (simp_all add: y_def inverse_eq_divide)
1.11      have "convergent (\<lambda>n. norm x *\<^sub>R X n y)"
1.12 @@ -301,7 +301,7 @@
1.13    have "X \<longlonglongrightarrow> Blinfun v"
1.14    proof (rule LIMSEQ_I)
1.15      fix r::real assume "r > 0"
1.16 -    def r' \<equiv> "r / 2"
1.17 +    define r' where "r' = r / 2"
1.18      have "0 < r'" "r' < r" using \<open>r > 0\<close> by (simp_all add: r'_def)
1.19      from CauchyD[OF \<open>Cauchy X\<close> \<open>r' > 0\<close>]
1.20      obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
```