diff -r 458068404143 -r ddd33e0f4935 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Wed Dec 13 09:39:53 2000 +0100 +++ b/doc-src/TutorialI/IsaMakefile Wed Dec 13 10:11:13 2000 +0100 @@ -113,7 +113,7 @@ $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \ Rules/Blast.thy Rules/Force.thy Rules/Primes.thy \ Rules/ROOT.ML - @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Rules + @$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Rules @rm -f tutorial.dvi ## HOL-Sets @@ -122,7 +122,7 @@ $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \ Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML - @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Sets + @$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Sets @rm -f tutorial.dvi ## HOL-CTL