1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:32:02 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 18:08:43 2011 -0700
     1.3 @@ -10,8 +10,8 @@
     1.4    "~~/src/HOL/Library/Infinite_Set"
     1.5    L2_Norm
     1.6    "~~/src/HOL/Library/Convex"
     1.7 +  "~~/src/HOL/Library/Sum_of_Squares"
     1.8  uses
     1.9 -  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
    1.10    ("normarith.ML")
    1.11  begin
    1.12