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