# HG changeset patch
# User huffman
# Date 1290908676 28800
# Node ID 4898bae6ef23aae7ffe7609f29ff04fa6d962b9a
# Parent  cce37f6d4b6964478c666fa2ef76c8d68096bccf
fix cut-and-paste errors for HOLCF entries in IsaMakefile

diff -r cce37f6d4b69 -r 4898bae6ef23 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Nov 27 17:29:21 2010 -0800
+++ b/src/HOL/IsaMakefile	Sat Nov 27 17:44:36 2010 -0800
@@ -1458,7 +1458,7 @@
   HOLCF/Tutorial/New_Domain.thy \
   HOLCF/Tutorial/document/root.tex \
   HOLCF/Tutorial/ROOT.ML
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
+	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
 
 
 ## HOLCF-Library
@@ -1479,9 +1479,12 @@
 
 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
 
-$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
-  HOLCF/IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
+$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF \
+  HOLCF/IMP/HoareEx.thy \
+  HOLCF/IMP/Denotational.thy \
+  HOLCF/IMP/ROOT.ML \
+  HOLCF/IMP/document/root.tex
+	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
 
 
 ## HOLCF-ex
@@ -1489,7 +1492,7 @@
 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
 
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
-  HOLCF/../HOL/Library/Nat_Infinity.thy \
+  Library/Nat_Infinity.thy \
   HOLCF/ex/Dagstuhl.thy \
   HOLCF/ex/Dnat.thy \
   HOLCF/ex/Domain_Proofs.thy \
@@ -1501,7 +1504,7 @@
   HOLCF/ex/Pattern_Match.thy \
   HOLCF/ex/Powerdomain_ex.thy \
   HOLCF/ex/ROOT.ML
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
+	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
 
 
 ## HOLCF-FOCUS
@@ -1511,10 +1514,14 @@
 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
   HOLCF/Library/Stream.thy \
   HOLCF/FOCUS/Fstreams.thy \
-  HOLCF/FOCUS/Fstream.thy FOCUS/FOCUS.thy \
-  HOLCF/FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
-  HOLCF/FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
+  HOLCF/FOCUS/Fstream.thy \
+  HOLCF/FOCUS/FOCUS.thy \
+  HOLCF/FOCUS/Stream_adm.thy \
+  HOLCF/FOCUS/Buffer.thy \
+  HOLCF/FOCUS/Buffer_adm.thy \
+  Library/Continuity.thy
+	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
+
 
 ## IOA
 
@@ -1544,6 +1551,7 @@
   HOLCF/IOA/meta_theory/SimCorrectness.thy
 	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
 
+
 ## IOA-ABP
 
 IOA-ABP: IOA $(LOG)/IOA-ABP.gz
@@ -1565,6 +1573,7 @@
   HOLCF/IOA/ABP/Spec.thy
 	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
 
+
 ## IOA-NTP
 
 IOA-NTP: IOA $(LOG)/IOA-NTP.gz