changeset 44287 | 598ed12b9bee |
parent 44286 | 8766839efb1b |
child 44360 | ea609ebdeebf |
--- 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