Corrected imports; better approximation of dependencies.
authorhoelzl
Tue May 04 18:19:24 2010 +0200 (2010-05-04)
changeset 36649bfd8c550faa6
parent 36648 43b66dcd9266
child 36650 d65f07abfa7c
Corrected imports; better approximation of dependencies.
src/HOL/IsaMakefile
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Product_Measure.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue May 04 18:05:22 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 04 18:19:24 2010 +0200
     1.3 @@ -1095,7 +1095,10 @@
     1.4    Multivariate_Analysis/Path_Connected.thy		\
     1.5    Multivariate_Analysis/Real_Integration.thy		\
     1.6    Multivariate_Analysis/Topology_Euclidean_Space.thy	\
     1.7 -  Multivariate_Analysis/Vec1.thy
     1.8 +  Multivariate_Analysis/Vec1.thy Library/Glbs.thy	\
     1.9 +  Library/Inner_Product.thy Library/Numeral_Type.thy	\
    1.10 +  Library/Convex.thy Library/FrechetDeriv.thy		\
    1.11 +  Library/Product_Vector.thy Library/Product_plus.thy
    1.12  	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis
    1.13  
    1.14  
    1.15 @@ -1109,7 +1112,10 @@
    1.16    Probability/Borel.thy Probability/Measure.thy			\
    1.17    Probability/Lebesgue.thy Probability/Product_Measure.thy	\
    1.18    Probability/Probability_Space.thy Probability/Information.thy \
    1.19 -  Probability/ex/Dining_Cryptographers.thy
    1.20 +  Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy	\
    1.21 +  Library/Convex.thy Library/Product_Vector.thy 		\
    1.22 +  Library/Product_plus.thy Library/Inner_Product.thy		\
    1.23 +  Library/Nat_Bijection.thy
    1.24  	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability
    1.25  
    1.26  
     2.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue May 04 18:05:22 2010 +0200
     2.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue May 04 18:19:24 2010 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  header {*Caratheodory Extension Theorem*}
     2.5  
     2.6  theory Caratheodory
     2.7 -  imports Sigma_Algebra SupInf SeriesPlus
     2.8 +  imports Sigma_Algebra SeriesPlus
     2.9  begin
    2.10  
    2.11  text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
     3.1 --- a/src/HOL/Probability/Information.thy	Tue May 04 18:05:22 2010 +0200
     3.2 +++ b/src/HOL/Probability/Information.thy	Tue May 04 18:19:24 2010 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  theory Information
     3.5 -imports Probability_Space Product_Measure "../Multivariate_Analysis/Convex"
     3.6 +imports Probability_Space Product_Measure Convex
     3.7  begin
     3.8  
     3.9  section "Convex theory"
     4.1 --- a/src/HOL/Probability/Product_Measure.thy	Tue May 04 18:05:22 2010 +0200
     4.2 +++ b/src/HOL/Probability/Product_Measure.thy	Tue May 04 18:19:24 2010 +0200
     4.3 @@ -1,5 +1,5 @@
     4.4  theory Product_Measure
     4.5 -imports "~~/src/HOL/Probability/Lebesgue"
     4.6 +imports Lebesgue
     4.7  begin
     4.8  
     4.9  definition