--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 29 09:29:47 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 29 11:41:04 2010 -0700
@@ -1090,7 +1090,7 @@
show "bounded_linear (g' x)" unfolding linear_linear linear_def apply(rule,rule,rule) defer proof(rule,rule)
fix x' y z::"real^'m" and c::real
note lin = assms(2)[rule_format,OF `x\<in>s`,THEN derivative_linear]
- show "g' x (c *s x') = c *s g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially])
+ show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially])
apply(rule lem3[rule_format]) unfolding smult_conv_scaleR
unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format]
apply(rule Lim_cmul) by(rule lem3[rule_format])