# HG changeset patch
# User huffman
# Date 1313716123 25200
# Node ID 598ed12b9bee534f4a796b9a371327afff0d3b58
# Parent  8766839efb1b90500817338139ae80229d03d1ad
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML

diff -r 8766839efb1b -r 598ed12b9bee src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:32:02 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 18:08:43 2011 -0700
@@ -10,8 +10,8 @@
   "~~/src/HOL/Library/Infinite_Set"
   L2_Norm
   "~~/src/HOL/Library/Convex"
+  "~~/src/HOL/Library/Sum_of_Squares"
 uses
-  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
   ("normarith.ML")
 begin