src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 09:37:46 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 09:45:22 2010 -0700
@@ -1381,7 +1381,7 @@
     apply(rule_tac x=x in bexI) apply assumption+ apply(rule continuous_on_intros)+
     unfolding frontier_cball subset_eq Ball_def image_iff apply(rule,rule,erule bexE)
     unfolding vector_dist_norm apply(simp add: * norm_minus_commute) . note x = this
-  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:group_simps)
+  hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:algebra_simps)
   hence "a = x" unfolding scaleR_left_distrib[THEN sym] by auto 
   thus False using x using assms by auto qed
 
@@ -1394,7 +1394,7 @@
  "interval_bij (a,b) (u,v) = (\<lambda>x. (\<chi> i. (v$i - u$i) / (b$i - a$i) * x$i) +
             (\<chi> i. u$i - (v$i - u$i) / (b$i - a$i) * a$i))"
   apply rule unfolding Cart_eq interval_bij_def vector_component_simps
-  by(auto simp add:group_simps field_simps add_divide_distrib[THEN sym]) 
+  by(auto simp add: field_simps add_divide_distrib[THEN sym]) 
 
 lemma continuous_interval_bij:
   "continuous (at x) (interval_bij (a,b::real^'n) (u,v))"