doc-src/TutorialI/IsaMakefile
changeset 11249 a0e3c67c1394
parent 11203 881222d48777
child 11279 aaa0ad8fea6b
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Tue Apr 10 16:09:26 2001 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Apr 10 16:11:01 2001 +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-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types 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-Real-Types HOL-Misc HOL-Protocol styles
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -170,7 +170,19 @@
    1.13  	@rm -f tutorial.dvi
    1.14  
    1.15  
    1.16 +## HOL-Protocol
    1.17 +
    1.18 +HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
    1.19 +
    1.20 +$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \
    1.21 +  Protocol/Message.thy Protocol/Message_lemmas.ML  \
    1.22 +  Protocol/Event.thy Protocol/Event_lemmas.ML  \
    1.23 +  Protocol/Public.thy Protocol/Public_lemmas.ML \
    1.24 +  Protocol/NS_Public.thy    
    1.25 +	$(USEDIR) Protocol
    1.26 +	@rm -f tutorial.dvi
    1.27 +
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 -	@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 $(LOG)/HOL-Types.gz
    1.32 +	@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 $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz