# HG changeset patch
# User paulson
# Date 979120817 -3600
# Node ID 28a53b68a8c0a320d4623c80976b6edef7307973
# Parent  1f93f5a27de6081f8f2c4b37dd8cedac6e4efb60
fixed the treatment of Rules and Sets

diff -r 1f93f5a27de6 -r 28a53b68a8c0 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed Jan 10 10:40:34 2001 +0100
+++ b/doc-src/TutorialI/IsaMakefile	Wed Jan 10 11:00:17 2001 +0100
@@ -115,9 +115,9 @@
 HOL-Rules: HOL $(LOG)/HOL-Rules.gz
 
 $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
-	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy  \
+	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy  \
 	Rules/ROOT.ML 
-	@$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Rules
+	@$(USEDIR) Rules
 	@rm -f tutorial.dvi
 
 ## HOL-Sets
@@ -126,7 +126,7 @@
 
 $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
 	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
-	@$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Sets
+	@$(USEDIR) Sets
 	@rm -f tutorial.dvi
 
 ## HOL-CTL