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/Library/FrechetDeriv.thy
changeset 34146 14595e0c27e8
parent 32960 69916a850301
child 36361 1debc8e29f6a 
--- a/src/HOL/Library/FrechetDeriv.thy	Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/Library/FrechetDeriv.thy	Fri Dec 18 19:00:11 2009 -0800
@@ -438,7 +438,7 @@
     hence 2: "x + h \<noteq> 0"
       apply (rule contrapos_nn)
       apply (rule sym)
-      apply (erule equals_zero_I)
+      apply (erule minus_unique)
       done
     show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h
           = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h"
isabelle