src/CTT/IsaMakefile
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 42138 e54a985daa61
child 45860 93eda35a8377
permissions -rw-r--r--
remove lemma stupid_ext
     1 #
     2 # IsaMakefile for CTT
     3 #
     4 
     5 ## targets
     6 
     7 default: CTT
     8 images: CTT
     9 test: CTT-ex
    10 all: images test
    11 smlnj: all
    12 
    13 
    14 ## global settings
    15 
    16 SRC = $(ISABELLE_HOME)/src
    17 OUT = $(ISABELLE_OUTPUT)
    18 LOG = $(OUT)/log
    19 
    20 
    21 ## CTT
    22 
    23 CTT: Pure $(OUT)/CTT
    24 
    25 Pure:
    26 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    27 
    28 $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
    29   Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
    30 	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT
    31 
    32 
    33 ## CTT-ex
    34 
    35 CTT-ex: CTT $(LOG)/CTT-ex.gz
    36 
    37 $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
    38   ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
    39 	@$(ISABELLE_TOOL) usedir $(OUT)/CTT ex
    40 
    41 
    42 ## clean
    43 
    44 clean:
    45 	@rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz