# HG changeset patch
# User huffman
# Date 1272519405 25200
# Node ID 8175a688c5e3bd2ba7eb28329934f5660fd62477
# Parent  534418d8d4948f4073ed2b02415d4000f3e018cd
generalize orthogonal_clauses

diff -r 534418d8d494 -r 8175a688c5e3 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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)"