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.
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
authorhoelzl
Wed, 01 Dec 2010 19:27:53 +0100
changeset 40860 a6df324752da
parent 40859 de0b30e6c2d2
child 40861 c888ab4b4ac7
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Wed Dec 01 19:20:30 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 01 19:27:53 2010 +0100
@@ -1156,7 +1156,7 @@
   Multivariate_Analysis/Finite_Cartesian_Product.thy			\
   Multivariate_Analysis/Integration.certs				\
   Multivariate_Analysis/Integration.thy					\
-  Multivariate_Analysis/Gauge_Measure.thy					\
+  Multivariate_Analysis/Gauge_Measure.thy				\
   Multivariate_Analysis/L2_Norm.thy					\
   Multivariate_Analysis/Multivariate_Analysis.thy			\
   Multivariate_Analysis/Operator_Norm.thy				\
@@ -1166,8 +1166,8 @@
   Multivariate_Analysis/Topology_Euclidean_Space.thy			\
   Multivariate_Analysis/document/root.tex				\
   Multivariate_Analysis/normarith.ML Library/Glbs.thy			\
-  Library/Inner_Product.thy Library/Numeral_Type.thy			\
-  Library/Convex.thy Library/FrechetDeriv.thy				\
+  Library/Indicator_Function.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 HOL-Multivariate_Analysis
 
@@ -1176,16 +1176,19 @@
 
 HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability
 
-$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis Probability/ROOT.ML	\
-  Probability/Probability.thy Probability/Sigma_Algebra.thy		\
-  Probability/Caratheodory.thy		\
-  Probability/Borel.thy Probability/Measure.thy				\
-  Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy		\
-  Probability/Positive_Infinite_Real.thy Probability/Product_Measure.thy	\
-  Probability/Probability_Space.thy Probability/Information.thy		\
-  Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy		\
-  Probability/Lebesgue_Measure.thy \
-  Library/Nat_Bijection.thy Library/Countable.thy
+$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis
+  Probability/Borel_Space.thy Probability/Caratheodory.thy		\
+  Probability/Complete_Measure.thy					\
+  Probability/ex/Dining_Cryptographers.thy				\
+  Probability/ex/Koepf_Duermuth_Countermeasure.thy			\
+  Probability/Information.thy Probability/Lebesgue_Integration.thy	\
+  Probability/Lebesgue_Measure.thy Probability/Measure.thy		\
+  Probability/Positive_Infinite_Real.thy				\
+  Probability/Probability_Space.thy Probability/Probability.thy		\
+  Probability/Product_Measure.thy Probability/Radon_Nikodym.thy		\
+  Probability/ROOT.ML Probability/Sigma_Algebra.thy			\
+  Library/Countable.thy Library/FuncSet.thy				\
+  Library/Nat_Bijection.thy
 	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
isabelle