# HG changeset patch
# User wenzelm
# Date 1469448149 -7200
# Node ID 6c2c16fef8f18663b8ed4a44d97c690c456a9df4
# Parent  00521f1815101bece776dc87e25443936c3181b9
unused (see 1e9e68247ad1);

diff -r 00521f181510 -r 6c2c16fef8f1 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Jul 25 11:30:31 2016 +0200
+++ b/src/HOL/Limits.thy	Mon Jul 25 14:02:29 2016 +0200
@@ -2080,24 +2080,6 @@
 qed
 
 
-subsubsection \<open>Cauchy Sequences are Bounded\<close>
-
-text \<open>
-  A Cauchy sequence is bounded -- this is the standard
-  proof mechanization rather than the nonstandard proof.
-\<close>
-
-lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real) \<Longrightarrow>
-  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
-  apply clarify
-  apply (drule spec)
-  apply (drule (1) mp)
-  apply (simp only: norm_minus_commute)
-  apply (drule order_le_less_trans [OF norm_triangle_ineq2])
-  apply simp
-  done
-
-
 subsection \<open>Power Sequences\<close>
 
 text \<open>