# HG changeset patch
# User hoelzl
# Date 1362585381 -3600
# Node ID c4367ed99b5ebee7e51e5d37c708df4867c48c14
# Parent  00b45c7e831f038b581cb0db0038418db7f767d0
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->

diff -r 00b45c7e831f -r c4367ed99b5e src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Mar 06 16:10:56 2013 +0100
+++ b/src/HOL/Limits.thy	Wed Mar 06 16:56:21 2013 +0100
@@ -775,15 +775,24 @@
   tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   "(f ---> l) F \<equiv> filterlim f (nhds l) F"
 
+lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
+  by simp
+
 ML {*
+
 structure Tendsto_Intros = Named_Thms
 (
   val name = @{binding tendsto_intros}
   val description = "introduction rules for tendsto"
 )
+
 *}
 
-setup Tendsto_Intros.setup
+setup {*
+  Tendsto_Intros.setup #>
+  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
+    map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
+*}
 
 lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   unfolding filterlim_def