nipkow@8743: # nipkow@8743: # IsaMakefile for Tutorial nipkow@8743: # nipkow@8743: nipkow@8743: ## targets nipkow@8743: wenzelm@11647: default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \ paulson@13977: HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \ wenzelm@11647: HOL-Protocol HOL-Documents styles wenzelm@9520: images: wenzelm@9520: test: wenzelm@9520: all: default nipkow@8743: nipkow@8743: nipkow@8743: ## global settings nipkow@8743: nipkow@8743: SRC = $(ISABELLE_HOME)/src nipkow@8743: OUT = $(ISABELLE_OUTPUT) nipkow@8743: LOG = $(OUT)/log nipkow@16069: OPTIONS = -H false -m brackets -i true -d "" -D document wenzelm@11617: USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL paulson@13977: REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex wenzelm@11617: nipkow@8743: nipkow@8743: ## HOL nipkow@8743: nipkow@8743: HOL: nipkow@8743: @cd $(SRC)/HOL; $(ISATOOL) make HOL nipkow@8743: paulson@13977: HOL-Complex: paulson@13977: @cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex paulson@10765: wenzelm@8825: styles: nipkow@10654: @rm -f isabelle.sty nipkow@10654: @rm -f isabellesym.sty nipkow@10654: @rm -f pdfsetup.sty wenzelm@8847: @$(ISATOOL) latex -o sty >/dev/null wenzelm@8847: @rm -f pdfsetup.sty wenzelm@8825: @rm -f */document/isabelle.sty wenzelm@8825: @rm -f */document/isabellesym.sty wenzelm@8825: @rm -f */document/pdfsetup.sty wenzelm@10002: @rm -f */document/session.tex paulson@11401: nipkow@8743: nipkow@8743: nipkow@8743: ## HOL-Ifexpr nipkow@8743: nipkow@8743: HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz nipkow@8743: nipkow@8743: $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML nipkow@10676: $(USEDIR) Ifexpr nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: ## HOL-ToyList nipkow@8743: nipkow@8743: HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz nipkow@8743: nipkow@8743: ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 nipkow@8743: cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy nipkow@8743: nipkow@8743: $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML nipkow@10676: $(USEDIR) ToyList2 nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML nipkow@10676: $(USEDIR) ToyList nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: ## HOL-CodeGen nipkow@8743: nipkow@8743: HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz nipkow@8743: nipkow@10676: $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy nipkow@10676: $(USEDIR) CodeGen nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: nipkow@8743: ## HOL-Datatype nipkow@8743: nipkow@8743: HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz nipkow@8743: nipkow@8751: $(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ nipkow@9666: Datatype/Nested.thy Datatype/unfoldnested.thy \ nipkow@9644: Datatype/Fundata.thy nipkow@10676: $(USEDIR) Datatype nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: nipkow@8743: ## HOL-Trie nipkow@8743: nipkow@8743: HOL-Trie: HOL $(LOG)/HOL-Trie.gz nipkow@8743: nipkow@10543: $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy nipkow@10676: $(USEDIR) Trie nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: nipkow@8743: ## HOL-Recdef nipkow@8743: nipkow@8743: HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz nipkow@8743: nipkow@10186: $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ nipkow@9644: Recdef/simplification.thy Recdef/Induction.thy \ nipkow@10187: Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy nipkow@10676: $(USEDIR) Recdef nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: nipkow@9933: ## HOL-Advanced nipkow@9933: nipkow@9933: HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz nipkow@9933: nipkow@10654: $(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \ nipkow@10654: Advanced/Partial.thy nipkow@10676: $(USEDIR) Advanced nipkow@9933: @rm -f tutorial.dvi nipkow@9933: paulson@10296: ## HOL-Rules paulson@10296: paulson@10296: HOL-Rules: HOL $(LOG)/HOL-Rules.gz paulson@10296: paulson@10296: $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \ paulson@10956: Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ nipkow@16543: Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML paulson@10840: @$(USEDIR) Rules paulson@10296: @rm -f tutorial.dvi paulson@10296: paulson@10296: ## HOL-Sets paulson@10296: paulson@10296: HOL-Sets: HOL $(LOG)/HOL-Sets.gz paulson@10296: paulson@10296: $(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \ paulson@10296: Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML paulson@10840: @$(USEDIR) Sets paulson@10296: @rm -f tutorial.dvi paulson@10296: nipkow@9958: ## HOL-CTL nipkow@9958: nipkow@9958: HOL-CTL: HOL $(LOG)/HOL-CTL.gz nipkow@9958: nipkow@10212: $(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML nipkow@10676: $(USEDIR) CTL nipkow@9958: @rm -f tutorial.dvi nipkow@9958: nipkow@10217: ## HOL-Inductive nipkow@10217: nipkow@10217: HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz nipkow@10217: nipkow@10225: $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ nipkow@10762: Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ nipkow@10762: Inductive/Advanced.thy nipkow@10676: $(USEDIR) Inductive nipkow@10217: @rm -f tutorial.dvi nipkow@10217: nipkow@10328: ## HOL-Types nipkow@10328: paulson@13977: HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz nipkow@10328: paulson@13977: $(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \ wenzelm@11858: Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \ nipkow@10328: Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ nipkow@10328: Types/Overloading.thy Types/Axioms.thy paulson@10765: $(REALUSEDIR) Types nipkow@10328: @rm -f tutorial.dvi nipkow@10328: nipkow@8743: ## HOL-Misc nipkow@8743: nipkow@8743: HOL-Misc: HOL $(LOG)/HOL-Misc.gz nipkow@8743: nipkow@9722: $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ nipkow@13305: Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \ nipkow@13305: Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \ nipkow@10978: Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy nipkow@10676: $(USEDIR) Misc nipkow@8754: @rm -f tutorial.dvi nipkow@8743: nipkow@8743: paulson@11249: ## HOL-Protocol paulson@11249: paulson@11249: HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz paulson@11249: paulson@11249: $(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \ paulson@11249: Protocol/Message.thy Protocol/Message_lemmas.ML \ paulson@11249: Protocol/Event.thy Protocol/Event_lemmas.ML \ paulson@11249: Protocol/Public.thy Protocol/Public_lemmas.ML \ paulson@11249: Protocol/NS_Public.thy paulson@11249: $(USEDIR) Protocol paulson@11249: @rm -f tutorial.dvi paulson@11249: wenzelm@11647: ## HOL-Documents wenzelm@11647: wenzelm@11647: HOL-Documents: HOL $(LOG)/HOL-Documents.gz wenzelm@11647: wenzelm@11647: $(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML wenzelm@11647: $(USEDIR) Documents wenzelm@11647: @rm -f tutorial.dvi wenzelm@11647: nipkow@8743: ## clean nipkow@8743: nipkow@8743: clean: wenzelm@11647: @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 $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex