# HG changeset patch
# User hoelzl
# Date 1272989964 -7200
# Node ID bfd8c550faa69d139eefb4b76901ea5ffc8ef67a
# Parent  43b66dcd926603da09317838590a9c18bb94093d
Corrected imports; better approximation of dependencies.

diff -r 43b66dcd9266 -r bfd8c550faa6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 04 18:05:22 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue May 04 18:19:24 2010 +0200
@@ -1095,7 +1095,10 @@
   Multivariate_Analysis/Path_Connected.thy		\
   Multivariate_Analysis/Real_Integration.thy		\
   Multivariate_Analysis/Topology_Euclidean_Space.thy	\
-  Multivariate_Analysis/Vec1.thy
+  Multivariate_Analysis/Vec1.thy Library/Glbs.thy	\
+  Library/Inner_Product.thy Library/Numeral_Type.thy	\
+  Library/Convex.thy Library/FrechetDeriv.thy		\
+  Library/Product_Vector.thy Library/Product_plus.thy
 	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
 
 
@@ -1109,7 +1112,10 @@
   Probability/Borel.thy Probability/Measure.thy			\
   Probability/Lebesgue.thy Probability/Product_Measure.thy	\
   Probability/Probability_Space.thy Probability/Information.thy \
-  Probability/ex/Dining_Cryptographers.thy
+  Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy	\
+  Library/Convex.thy Library/Product_Vector.thy 		\
+  Library/Product_plus.thy Library/Inner_Product.thy		\
+  Library/Nat_Bijection.thy
 	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability
 
 
diff -r 43b66dcd9266 -r bfd8c550faa6 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Tue May 04 18:05:22 2010 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Tue May 04 18:19:24 2010 +0200
@@ -1,7 +1,7 @@
 header {*Caratheodory Extension Theorem*}
 
 theory Caratheodory
-  imports Sigma_Algebra SupInf SeriesPlus
+  imports Sigma_Algebra SeriesPlus
 begin
 
 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
diff -r 43b66dcd9266 -r bfd8c550faa6 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Tue May 04 18:05:22 2010 +0200
+++ b/src/HOL/Probability/Information.thy	Tue May 04 18:19:24 2010 +0200
@@ -1,5 +1,5 @@
 theory Information
-imports Probability_Space Product_Measure "../Multivariate_Analysis/Convex"
+imports Probability_Space Product_Measure Convex
 begin
 
 section "Convex theory"
diff -r 43b66dcd9266 -r bfd8c550faa6 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Tue May 04 18:05:22 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy	Tue May 04 18:19:24 2010 +0200
@@ -1,5 +1,5 @@
 theory Product_Measure
-imports "~~/src/HOL/Probability/Lebesgue"
+imports Lebesgue
 begin
 
 definition