src/HOL/NthRoot.thy
changeset 63040 eb4ddd18d635
parent 62393 a620a8756b7c
child 63367 6c731c8b7f03
     1.1 --- a/src/HOL/NthRoot.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -646,7 +646,7 @@
     1.4  
     1.5  lemma LIMSEQ_root: "(\<lambda>n. root n n) \<longlonglongrightarrow> 1"
     1.6  proof -
     1.7 -  def x \<equiv> "\<lambda>n. root n n - 1"
     1.8 +  define x where "x n = root n n - 1" for n
     1.9    have "x \<longlonglongrightarrow> sqrt 0"
    1.10    proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    1.11      show "(\<lambda>x. sqrt (2 / x)) \<longlonglongrightarrow> sqrt 0"
    1.12 @@ -684,7 +684,7 @@
    1.13    shows "(\<lambda>n. root n c) \<longlonglongrightarrow> 1"
    1.14  proof -
    1.15    { fix c :: real assume "1 \<le> c"
    1.16 -    def x \<equiv> "\<lambda>n. root n c - 1"
    1.17 +    define x where "x n = root n c - 1" for n
    1.18      have "x \<longlonglongrightarrow> 0"
    1.19      proof (rule tendsto_sandwich[OF _ _ tendsto_const])
    1.20        show "(\<lambda>n. c / n) \<longlonglongrightarrow> 0"