1.1 --- a/src/HOL/IsaMakefile Sat Nov 27 17:29:21 2010 -0800
1.2 +++ b/src/HOL/IsaMakefile Sat Nov 27 17:44:36 2010 -0800
1.3 @@ -1458,7 +1458,7 @@
1.4 HOLCF/Tutorial/New_Domain.thy \
1.5 HOLCF/Tutorial/document/root.tex \
1.6 HOLCF/Tutorial/ROOT.ML
1.7 - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
1.8 + @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
1.9
1.10
1.11 ## HOLCF-Library
1.12 @@ -1479,9 +1479,12 @@
1.13
1.14 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
1.15
1.16 -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
1.17 - HOLCF/IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
1.18 - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
1.19 +$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF \
1.20 + HOLCF/IMP/HoareEx.thy \
1.21 + HOLCF/IMP/Denotational.thy \
1.22 + HOLCF/IMP/ROOT.ML \
1.23 + HOLCF/IMP/document/root.tex
1.24 + @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
1.25
1.26
1.27 ## HOLCF-ex
1.28 @@ -1489,7 +1492,7 @@
1.29 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
1.30
1.31 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
1.32 - HOLCF/../HOL/Library/Nat_Infinity.thy \
1.33 + Library/Nat_Infinity.thy \
1.34 HOLCF/ex/Dagstuhl.thy \
1.35 HOLCF/ex/Dnat.thy \
1.36 HOLCF/ex/Domain_Proofs.thy \
1.37 @@ -1501,7 +1504,7 @@
1.38 HOLCF/ex/Pattern_Match.thy \
1.39 HOLCF/ex/Powerdomain_ex.thy \
1.40 HOLCF/ex/ROOT.ML
1.41 - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
1.42 + @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
1.43
1.44
1.45 ## HOLCF-FOCUS
1.46 @@ -1511,10 +1514,14 @@
1.47 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
1.48 HOLCF/Library/Stream.thy \
1.49 HOLCF/FOCUS/Fstreams.thy \
1.50 - HOLCF/FOCUS/Fstream.thy FOCUS/FOCUS.thy \
1.51 - HOLCF/FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
1.52 - HOLCF/FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
1.53 - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
1.54 + HOLCF/FOCUS/Fstream.thy \
1.55 + HOLCF/FOCUS/FOCUS.thy \
1.56 + HOLCF/FOCUS/Stream_adm.thy \
1.57 + HOLCF/FOCUS/Buffer.thy \
1.58 + HOLCF/FOCUS/Buffer_adm.thy \
1.59 + Library/Continuity.thy
1.60 + @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
1.61 +
1.62
1.63 ## IOA
1.64
1.65 @@ -1544,6 +1551,7 @@
1.66 HOLCF/IOA/meta_theory/SimCorrectness.thy
1.67 @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
1.68
1.69 +
1.70 ## IOA-ABP
1.71
1.72 IOA-ABP: IOA $(LOG)/IOA-ABP.gz
1.73 @@ -1565,6 +1573,7 @@
1.74 HOLCF/IOA/ABP/Spec.thy
1.75 @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
1.76
1.77 +
1.78 ## IOA-NTP
1.79
1.80 IOA-NTP: IOA $(LOG)/IOA-NTP.gz