src/FOL/IsaMakefile
author wenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 47022 8eac39af4ec0
parent 45860 93eda35a8377
permissions -rw-r--r--
moved some legacy stuff;
     1 #
     2 # IsaMakefile for FOL
     3 #
     4 
     5 ## targets
     6 
     7 default: FOL
     8 images: FOL
     9 test: FOL-ex
    10 all: images test
    11 full: all
    12 smlnj: all
    13 
    14 
    15 ## global settings
    16 
    17 SRC = $(ISABELLE_HOME)/src
    18 OUT = $(ISABELLE_OUTPUT)
    19 LOG = $(OUT)/log
    20 
    21 
    22 ## FOL
    23 
    24 FOL: Pure $(OUT)/FOL
    25 
    26 Pure:
    27 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    28 
    29 $(OUT)/Pure: Pure
    30 
    31 $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
    32   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    33   $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML		\
    34   $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
    35   $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
    36   $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
    37   $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
    38   $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
    39   $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    40   $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
    41   document/root.tex fologic.ML intprover.ML simpdata.ML
    42 	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
    43 
    44 
    45 ## FOL-ex
    46 
    47 FOL-ex: FOL $(LOG)/FOL-ex.gz
    48 
    49 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
    50   ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy			\
    51   ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy	\
    52   ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy	\
    53   ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
    54   ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
    55   ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\
    56   ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
    57 	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
    58 
    59 
    60 ## clean
    61 
    62 clean:
    63 	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz