src/Sequents/IsaMakefile
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 36862 952b2b102a0a
child 42138 e54a985daa61
permissions -rw-r--r--
storing options for prolog code generation in the theory
     1 #
     2 # IsaMakefile for Sequents
     3 #
     4 
     5 ## targets
     6 
     7 default: Sequents
     8 images: Sequents
     9 test: Sequents-LK
    10 all: images test
    11 
    12 
    13 ## global settings
    14 
    15 SRC = $(ISABELLE_HOME)/src
    16 OUT = $(ISABELLE_OUTPUT)
    17 LOG = $(OUT)/log
    18 
    19 
    20 ## Sequents
    21 
    22 Sequents: Pure $(OUT)/Sequents
    23 
    24 Pure:
    25 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    26 
    27 $(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
    28   modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
    29   ILL_predlog.thy Washing.thy
    30 	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure Sequents
    31 
    32 
    33 ## Sequents-LK
    34 
    35 Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
    36 
    37 $(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \
    38   LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy
    39 	@$(ISABELLE_TOOL) usedir $(OUT)/Sequents LK
    40 
    41 
    42 ## clean
    43 
    44 clean:
    45 	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-LK.gz