diff -r 12378df46752 -r 9dd394c866fc src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Oct 01 23:26:31 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Oct 02 15:07:41 2015 +0100
@@ -1908,9 +1908,6 @@
 
 text \<open>Picking an orthogonal replacement for a spanning set.\<close>
 
-(* FIXME : Move to some general theory ?*)
-definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
-
 lemma vector_sub_project_orthogonal:
   fixes b x :: "'a::euclidean_space"
   shows "b \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"