Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
authorhuffman
Thu, 18 Aug 2011 18:08:43 -0700
changeset 44287 598ed12b9bee
parent 44286 8766839efb1b
child 44288 fe9c2398c330
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
src/HOL/Multivariate_Analysis/Linear_Algebra.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle