src/HOL/Transcendental.thy
changeset 51477 2990382dc066
parent 50347 77e3effa50b6
child 51478 270b21f3ae0a
     1.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -207,7 +207,7 @@
     1.4      thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
     1.5    qed
     1.6    ultimately
     1.7 -  show ?thesis by (rule lemma_nest_unique)
     1.8 +  show ?thesis by (rule nested_sequence_unique)
     1.9  qed
    1.10  
    1.11  lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real"