#
# IsaMakefile for Tutorial
#
## targets
default: HOL-Tutorial HOL-ToyList2
images:
test:
all: default
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
OPTIONS = -m brackets -i true -d "" -D document -M 1
USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS)
## HOL
HOL:
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
## HOL-Tutorial
HOL-Tutorial: HOL $(LOG)/HOL-Tutorial.gz
$(LOG)/HOL-Tutorial.gz: $(OUT)/HOL ROOT.ML Ifexpr/Ifexpr.thy \
ToyList2/ToyList.thy CodeGen/CodeGen.thy Datatype/ABexpr.thy \
Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy \
Trie/Trie.thy Fun/fun0.thy Advanced/simp2.thy Rules/Basic.thy \
Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
Rules/Tacticals.thy Rules/find2.thy Sets/Examples.thy \
Sets/Functions.thy Sets/Recur.thy Sets/Relations.thy CTL/Base.thy \
CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy Inductive/Even.thy \
Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
Inductive/Advanced.thy Types/Numbers.thy Types/Pairs.thy \
Types/Records.thy Types/Typedefs.thy Types/Overloading.thy \
Types/Axioms.thy Misc/Tree.thy Misc/Tree2.thy Misc/Plus.thy \
Misc/fakenat.thy Misc/natsum.thy Misc/pairs2.thy Misc/Option2.thy \
Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy Misc/simp.thy \
Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy \
Protocol/Message.thy Protocol/Event.thy Protocol/Public.thy \
Protocol/NS_Public.thy Documents/Documents.thy
$(USEDIR) -s Tutorial $(OUT)/HOL .
## HOL-ToyList2
HOL-ToyList2: HOL $(LOG)/HOL-ToyList2.gz
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ROOT.ML
$(USEDIR) $(OUT)/HOL ToyList2
## clean
clean:
@rm -f tutorial.dvi $(LOG)/HOL-Tutorial.gz $(LOG)/HOL-ToyList2.gz