Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Corrected imports; better approximation of dependencies.
authorhoelzl
Tue, 04 May 2010 18:19:24 +0200
changeset 36649 bfd8c550faa6
parent 36648 43b66dcd9266
child 36650 d65f07abfa7c
Corrected imports; better approximation of dependencies.
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Probability/Caratheodory.thy file | annotate | diff | comparison | revisions
src/HOL/Probability/Information.thy file | annotate | diff | comparison | revisions
src/HOL/Probability/Product_Measure.thy file | annotate | diff | comparison | revisions 
--- 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
 
 
--- 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.*}
--- 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"
--- 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
isabelle