Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Deriv.thy
changeset 44314 dbad46932536
parent 44233 aa74ce315bae
child 44317 b7e9fa025f15 
--- a/src/HOL/Deriv.thy	Fri Aug 19 15:07:10 2011 -0700
+++ b/src/HOL/Deriv.thy	Fri Aug 19 15:54:43 2011 -0700
@@ -524,7 +524,7 @@
                 ((\<forall>n. l \<le> g(n)) & g ----> l)"
 apply (drule lemma_nest, auto)
 apply (subgoal_tac "l = m")
-apply (drule_tac [2] X = f in LIMSEQ_diff)
+apply (drule_tac [2] f = f in LIMSEQ_diff)
 apply (auto intro: LIMSEQ_unique)
 done
isabelle