author | huffman |
Thu, 18 Aug 2011 18:08:43 -0700 | |
changeset 44287 | 598ed12b9bee |
parent 44286 | 8766839efb1b |
child 44288 | fe9c2398c330 |
--- 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