--- 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
--- 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"
--- 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)"