--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 22:20:59 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Apr 28 22:36:45 2010 -0700
@@ -1208,9 +1208,8 @@
shows "orthogonal (basis i :: real^'n) (basis j) \<longleftrightarrow> i \<noteq> j"
unfolding orthogonal_basis[of i] basis_component[of j] by simp
- (* FIXME : Maybe some of these require less than comm_ring, but not all*)
lemma orthogonal_clauses:
- "orthogonal a (0::real ^'n)"
+ "orthogonal a 0"
"orthogonal a x ==> orthogonal a (c *\<^sub>R x)"
"orthogonal a x ==> orthogonal a (-x)"
"orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)"