--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Sep 26 16:33:32 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Sep 26 16:33:34 2013 -0700
@@ -106,7 +106,7 @@
from `0 < e` have "y \<noteq> x"
unfolding y_def by (auto intro!: nonzero_Basis)
from `0 < e` have "dist y x < e"
- unfolding y_def by (simp add: dist_norm norm_Basis)
+ unfolding y_def by (simp add: dist_norm)
from `y \<noteq> x` and `dist y x < e` show "False"
using e by simp
qed
@@ -123,7 +123,7 @@
[simp]: "Basis = {1::real}"
instance
- by default (auto simp add: Basis_real_def)
+ by default auto
end