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