# HG changeset patch
# User haftmann
# Date 1277731946 -7200
# Node ID b47dd044a1f18938b1e7a3924368cef916543d12
# Parent  625bc011768a817a0bd2ff8b10283eec023533d4
inner_simps is not enough, need also local facts

diff -r 625bc011768a -r b47dd044a1f1 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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
diff -r 625bc011768a -r b47dd044a1f1 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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"