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