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 30729 461ee3e49ad3
parent 30663 0b6aff7451b2
child 31021 53642251a04f 
--- a/src/HOL/Library/FrechetDeriv.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -222,8 +222,8 @@
   let ?k = "\<lambda>h. f (x + h) - f x"
   let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
   let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
-  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
-  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
+  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
+  from g interpret G: bounded_linear "G" by (rule FDERIV_bounded_linear)
   from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
   from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
isabelle