1 

     2 ## targets

     3 

     4 default: Quot

     5 images: 

     6 

     7 all: Quot

     8 

     9 

    10 ## global settings

    11 

    12 SRC = $(ISABELLE_HOME)/src

    13 OUT = $(ISABELLE_OUTPUT)

    14 LOG = $(OUT)/log

    15 

    16 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ##-D generated

    17 

    18 

    19 ## Quot

    20 

    21 Quot: $(LOG)/HOL-Quot.gz

    22 

    23 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy

    24 	@$(USEDIR) HOL-Nominal Quot

    25 

    26 paper: $(LOG)/HOL-Quot-Paper.gz

    27 

    28 $(LOG)/HOL-Quot-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy

    29 	@$(USEDIR) -D generated HOL Paper

    30 	$(ISATOOL) document -o pdf  Paper/generated

    31 	@cp Paper/document.pdf paper.pdf

    32 

    33 keywords:

    34 	mkdir -p tmp

    35 	cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/Pure.gz tmp 

    36 	cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/HOL.gz tmp

    37 	cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/Pure-ProofGeneral.gz tmp

    38 	cp $(ISABELLE_HOME)/heaps/polyml-5.3.0_x86-linux/log/HOL-Nominal.gz tmp

    39 	cp $(LOG)/HOL-Nominal-Quot.gz tmp

    40 	isabelle keywords -k quot tmp/*

    41 	

    42 	

    43 ## clean

    44 

    45 clean:

    46 	@rm -f $(LOG)/HOL-Quot.gz