# HG changeset patch
# User wenzelm
# Date 1280846916 -7200
# Node ID bd4965bb7bdc70e1bebd4a80338f70f8f97e4b1f
# Parent  2b9bfa0b44f194cc707e1d965c6fb017b6852d82
tuned headers -- more precise load path;

diff -r 2b9bfa0b44f1 -r bd4965bb7bdc src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Aug 03 16:33:11 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Aug 03 16:48:36 2010 +0200
@@ -5,8 +5,8 @@
 header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
 
 theory Parametric_Ferrante_Rackoff
-imports Reflected_Multivariate_Polynomial 
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports Reflected_Multivariate_Polynomial
+  Dense_Linear_Order
   Efficient_Nat
 begin
 
diff -r 2b9bfa0b44f1 -r bd4965bb7bdc src/HOL/Library/Sum_Of_Squares.thy
--- a/src/HOL/Library/Sum_Of_Squares.thy	Tue Aug 03 16:33:11 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Tue Aug 03 16:48:36 2010 +0200
@@ -7,9 +7,9 @@
   multiplication and ordering using semidefinite programming *}
 
 theory Sum_Of_Squares
-imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
+imports Complex_Main
 uses
-  "positivstellensatz.ML"  (* duplicate use!? -- cf. Euclidian_Space.thy *)
+  "positivstellensatz.ML"
   "Sum_Of_Squares/sum_of_squares.ML"
   "Sum_Of_Squares/positivstellensatz_tools.ML"
   "Sum_Of_Squares/sos_wrapper.ML"
diff -r 2b9bfa0b44f1 -r bd4965bb7bdc src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 03 16:33:11 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 03 16:48:36 2010 +0200
@@ -7,9 +7,10 @@
 theory Euclidean_Space
 imports
   Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  Infinite_Set
-  Inner_Product L2_Norm Convex
-uses "positivstellensatz.ML" ("normarith.ML")
+  Infinite_Set Inner_Product L2_Norm Convex
+uses
+  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
+  ("normarith.ML")
 begin
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"