1.1 --- a/src/HOL/IsaMakefile Tue Mar 23 17:26:41 2010 +0100
1.2 +++ b/src/HOL/IsaMakefile Tue Mar 23 19:35:03 2010 +0100
1.3 @@ -10,13 +10,14 @@
1.4 images: \
1.5 HOL \
1.6 HOL-Algebra \
1.7 + HOL-Base \
1.8 HOL-Boogie \
1.9 - HOL-Base \
1.10 HOL-Main \
1.11 HOL-Multivariate_Analysis \
1.12 HOL-NSA \
1.13 HOL-Nominal \
1.14 HOL-Plain \
1.15 + HOL-Probability \
1.16 HOL-Proofs \
1.17 HOL-SMT \
1.18 HOL-Word \
1.19 @@ -54,7 +55,6 @@
1.20 HOL-Number_Theory \
1.21 HOL-Old_Number_Theory \
1.22 HOL-Quotient_Examples \
1.23 - HOL-Probability \
1.24 HOL-Prolog \
1.25 HOL-Proofs-Extraction \
1.26 HOL-Proofs-Lambda \
1.27 @@ -1084,17 +1084,13 @@
1.28
1.29 ## HOL-Probability
1.30
1.31 -HOL-Probability: HOL $(LOG)/HOL-Probability.gz
1.32 +HOL-Probability: HOL $(OUT)/HOL-Probability
1.33
1.34 -$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \
1.35 - Probability/Probability.thy \
1.36 - Probability/Sigma_Algebra.thy \
1.37 - Probability/SeriesPlus.thy \
1.38 - Probability/Caratheodory.thy \
1.39 - Probability/Borel.thy \
1.40 - Probability/Measure.thy \
1.41 - Probability/Lebesgue.thy \
1.42 - Probability/Product_Measure.thy \
1.43 +$(OUT)/HOL-Probability: $(OUT)/HOL Probability/ROOT.ML \
1.44 + Probability/Probability.thy Probability/Sigma_Algebra.thy \
1.45 + Probability/SeriesPlus.thy Probability/Caratheodory.thy \
1.46 + Probability/Borel.thy Probability/Measure.thy \
1.47 + Probability/Lebesgue.thy Probability/Product_Measure.thy \
1.48 Probability/Probability_Space.thy
1.49 @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Probability
1.50
1.51 @@ -1316,12 +1312,12 @@
1.52 $(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz \
1.53 $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
1.54 $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
1.55 - $(LOG)/HOL-Word-Examples.gz \
1.56 - $(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \
1.57 - $(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz \
1.58 - $(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \
1.59 - $(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base \
1.60 - $(OUT)/HOL-Boogie $(OUT)/HOL-Main \
1.61 - $(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA \
1.62 - $(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-Proofs \
1.63 + $(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
1.64 + $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \
1.65 + $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \
1.66 + $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \
1.67 + $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \
1.68 + $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \
1.69 + $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
1.70 + $(OUT)/HOL-Probability $(OUT)/HOL-Proofs \
1.71 $(OUT)/HOL-SMT $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA