src/FOL/IsaMakefile
author wenzelm
Thu May 31 20:55:29 2007 +0200 (2007-05-31)
changeset 23171 861f63a35d31
parent 22822 c1a6a2159e69
child 23914 3e0424305fa4
permissions -rw-r--r--
moved IsaPlanner from Provers to Tools;
wenzelm@2433
     1
#
wenzelm@2433
     2
# $Id$
wenzelm@2433
     3
#
wenzelm@2433
     4
# IsaMakefile for FOL
wenzelm@2433
     5
#
wenzelm@2433
     6
wenzelm@4518
     7
## targets
wenzelm@4518
     8
wenzelm@4518
     9
default: FOL
wenzelm@4518
    10
images: FOL
wenzelm@4518
    11
test: FOL-ex
wenzelm@4518
    12
all: images test
wenzelm@4518
    13
wenzelm@4518
    14
wenzelm@4518
    15
## global settings
wenzelm@4518
    16
wenzelm@4518
    17
SRC = $(ISABELLE_HOME)/src
wenzelm@3118
    18
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    19
LOG = $(OUT)/log
wenzelm@2433
    20
paulson@3233
    21
wenzelm@4518
    22
## FOL
wenzelm@4518
    23
wenzelm@17821
    24
FOL: Pure $(OUT)/FOL$(ML_SUFFIX)
wenzelm@2433
    25
wenzelm@4518
    26
Pure:
wenzelm@4518
    27
	@cd $(SRC)/Pure; $(ISATOOL) make Pure
wenzelm@2433
    28
wenzelm@17821
    29
$(OUT)/Pure$(ML_SUFFIX): Pure
kleing@13301
    30
wenzelm@18482
    31
$(OUT)/FOL$(ML_SUFFIX): $(OUT)/Pure$(ML_SUFFIX) $(SRC)/Provers/blast.ML	\
wenzelm@16019
    32
  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
wenzelm@23171
    33
  $(SRC)/Tools/IsaPlanner/zipper.ML \
wenzelm@23171
    34
  $(SRC)/Tools/IsaPlanner/isand.ML \
wenzelm@23171
    35
  $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
wenzelm@23171
    36
  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
wenzelm@16019
    37
  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
wenzelm@22822
    38
  $(SRC)/Provers/induct_method.ML			\
wenzelm@18529
    39
  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
wenzelm@21539
    40
  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML 		\
wenzelm@18596
    41
  document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
wenzelm@18203
    42
	@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
wenzelm@2433
    43
wenzelm@4518
    44
wenzelm@4518
    45
## FOL-ex
wenzelm@4518
    46
wenzelm@4518
    47
FOL-ex: FOL $(LOG)/FOL-ex.gz
wenzelm@2433
    48
wenzelm@17821
    49
$(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \
wenzelm@22822
    50
  ex/If.thy ex/IffOracle.thy ex/LocaleTest.thy \
wenzelm@22822
    51
  ex/Nat.thy ex/Natural_Numbers.thy ex/Miniscope.thy \
wenzelm@19820
    52
  ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex \
wenzelm@19819
    53
  ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy ex/prop.ML ex/quant.ML
wenzelm@2821
    54
	@$(ISATOOL) usedir $(OUT)/FOL ex
wenzelm@2433
    55
wenzelm@4518
    56
wenzelm@4518
    57
## clean
wenzelm@4447
    58
wenzelm@4447
    59
clean:
wenzelm@17821
    60
	@rm -f $(OUT)/FOL$(ML_SUFFIX) $(LOG)/FOL.gz $(LOG)/FOL-ex.gz