Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
now includes Rules, Sets (?)
authorpaulson
Mon, 23 Oct 2000 17:35:17 +0200
changeset 102960c5907082459
parent 10295 8eb12693cead
child 10297 ab5617c3cefb
now includes Rules, Sets (?)
doc-src/TutorialI/IsaMakefile file | annotate | diff | comparison | revisions 
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Mon Oct 23 16:25:04 2000 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Mon Oct 23 17:35:17 2000 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  ## targets
     1.6  
     1.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Inductive HOL-Misc styles
     1.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Misc styles
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -102,6 +102,25 @@
    1.13  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
    1.14  	@rm -f tutorial.dvi
    1.15  
    1.16 +## HOL-Rules
    1.17 +
    1.18 +HOL-Rules: HOL $(LOG)/HOL-Rules.gz
    1.19 +
    1.20 +$(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
    1.21 +	Rules/Blast.thy Rules/Force.thy Rules/Primes.thy  \
    1.22 +	Rules/ROOT.ML 
    1.23 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Rules
    1.24 +	@rm -f tutorial.dvi
    1.25 +
    1.26 +## HOL-Sets
    1.27 +
    1.28 +HOL-Sets: HOL $(LOG)/HOL-Sets.gz
    1.29 +
    1.30 +$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
    1.31 +	Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
    1.32 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Sets
    1.33 +	@rm -f tutorial.dvi
    1.34 +
    1.35  ## HOL-CTL
    1.36  
    1.37  HOL-CTL: HOL $(LOG)/HOL-CTL.gz
    1.38 @@ -115,7 +134,7 @@
    1.39  HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
    1.40  
    1.41  $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
    1.42 -  Inductive/Star.thy Inductive/AB.thy
    1.43 +  Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Acc.thy
    1.44  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
    1.45  	@rm -f tutorial.dvi
    1.46  
    1.47 @@ -135,4 +154,4 @@
    1.48  ## clean
    1.49  
    1.50  clean:
    1.51 -	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz
    1.52 +	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz
wneuper/isa