src/HOL/Library/FrechetDeriv.thy

   let ?Rf = "\<lambda>h. f (x + h) - f x - F h"
   let ?Rg = "\<lambda>k. g (f x + k) - g (f x) - G k"
   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
 
   let ?fun2 = "\<lambda>h. ?Nf h * kG + ?Ng h * (?Nf h + kF)"