--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jun 28 15:32:26 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jun 28 15:32:26 2010 +0200
@@ -707,7 +707,7 @@
case False
have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add: power2_eq_square)
also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
- also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
+ also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by (auto simp add: inner_diff_left)
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
finally show ?thesis using False x(1) by(auto simp add: real_mult_left_cancel) next
case True thus ?thesis using assms(1) apply(rule_tac x="(a + b) /2" in bexI) by auto qed qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jun 28 15:32:26 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jun 28 15:32:26 2010 +0200
@@ -15,7 +15,7 @@
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
by auto
-abbreviation inner_bullet (infix "\<bullet>" 70) where "x \<bullet> y \<equiv> inner x y"
+notation inner (infix "\<bullet>" 70)
subsection {* A connectedness or intermediate value lemma with several applications. *}
@@ -466,8 +466,8 @@
"orthogonal x a \<Longrightarrow> orthogonal (-x) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
- unfolding orthogonal_def inner_simps by auto
-
+ unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
+
end
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"