# HG changeset patch
# User huffman
# Date 1291136327 28800
# Node ID ab0a8cc7976a848373f44cfa83fed5b2a11da01f
# Parent  142f890ceef67bee0432cda98c98946ed6cb2c24
simplify proof of LIMSEQ_unique

diff -r 142f890ceef6 -r ab0a8cc7976a src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Nov 30 08:35:04 2010 -0800
+++ b/src/HOL/SEQ.thy	Tue Nov 30 08:58:47 2010 -0800
@@ -221,15 +221,7 @@
 lemma LIMSEQ_unique:
   fixes a b :: "'a::metric_space"
   shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
-apply (rule ccontr)
-apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
-apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
-apply (clarify, rename_tac M N)
-apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
-apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
-apply (erule le_less_trans, rule add_strict_mono, simp, simp)
-apply (subst dist_commute, rule dist_triangle)
-done
+by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
 
 lemma (in bounded_linear) LIMSEQ:
   "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"