fixed the treatment of Rules and Sets
authorpaulson
Wed, 10 Jan 2001 11:00:17 +0100
changeset 1084028a53b68a8c0
parent 10839 1f93f5a27de6
child 10841 2fb8089ab6cd
fixed the treatment of Rules and Sets
doc-src/TutorialI/IsaMakefile
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Jan 10 10:40:34 2001 +0100
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Jan 10 11:00:17 2001 +0100
     1.3 @@ -115,9 +115,9 @@
     1.4  HOL-Rules: HOL $(LOG)/HOL-Rules.gz
     1.5  
     1.6  $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
     1.7 -	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy  \
     1.8 +	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy  \
     1.9  	Rules/ROOT.ML 
    1.10 -	@$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Rules
    1.11 +	@$(USEDIR) Rules
    1.12  	@rm -f tutorial.dvi
    1.13  
    1.14  ## HOL-Sets
    1.15 @@ -126,7 +126,7 @@
    1.16  
    1.17  $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
    1.18  	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
    1.19 -	@$(ISATOOL) usedir -d dvi -D document $(OUT)/HOL Sets
    1.20 +	@$(USEDIR) Sets
    1.21  	@rm -f tutorial.dvi
    1.22  
    1.23  ## HOL-CTL