1.1 --- a/src/HOL/IsaMakefile Sun Apr 01 23:09:36 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Sun Apr 01 23:21:54 2012 +0200
1.3 @@ -548,7 +548,7 @@
1.4 @$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
1.5
1.6
1.7 -## Import sessions
1.8 +## HOL-Import
1.9
1.10 HOL-Import: $(LOG)/HOL-Import.gz
1.11
1.12 @@ -561,6 +561,7 @@
1.13 Import/HOL_Light_Import.thy
1.14 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
1.15
1.16 +
1.17 ## HOL-Number_Theory
1.18
1.19 HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
1.20 @@ -1785,9 +1786,10 @@
1.21 @rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \
1.22 $(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \
1.23 $(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz \
1.24 - $(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz \
1.25 - $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz \
1.26 - $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \
1.27 + $(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-HOL_Light.gz \
1.28 + $(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz \
1.29 + $(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz \
1.30 + $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \
1.31 $(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \
1.32 $(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz \
1.33 $(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \
1.34 @@ -1817,18 +1819,17 @@
1.35 $(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz \
1.36 $(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz \
1.37 $(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \
1.38 - $(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz \
1.39 - $(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \
1.40 - $(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base \
1.41 - $(OUT)/HOL-Boogie $(OUT)/HOL-IMP $(OUT)/HOL-Library \
1.42 + $(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \
1.43 + $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \
1.44 + $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \
1.45 + $(OUT)/HOL-HOL_Light $(OUT)/HOL-IMP $(OUT)/HOL-Library \
1.46 $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \
1.47 $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
1.48 $(OUT)/HOL-Probability $(OUT)/HOL-Proofs \
1.49 - $(OUT)/HOL-SPARK $(OUT)/HOL-Word \
1.50 - $(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz \
1.51 - $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz \
1.52 - $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz \
1.53 - $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
1.54 + $(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/TLA \
1.55 + $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
1.56 + $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
1.57 + $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
1.58 $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \
1.59 $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz \
1.60 $(LOG)/HOL-Datatype_Benchmark.gz \