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'"