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;
wenzelm@2433
     1
#
wenzelm@2433
     2
# IsaMakefile for FOL
wenzelm@2433
     3
#
wenzelm@2433
     4
wenzelm@4518
     5
## targets
wenzelm@4518
     6
wenzelm@4518
     7
default: FOL
wenzelm@4518
     8
images: FOL
wenzelm@4518
     9
test: FOL-ex
wenzelm@4518
    10
all: images test
wenzelm@45860
    11
full: all
krauss@42138
    12
smlnj: all
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@27203
    24
FOL: Pure $(OUT)/FOL
wenzelm@2433
    25
wenzelm@4518
    26
Pure:
wenzelm@28500
    27
	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
wenzelm@2433
    28
wenzelm@27203
    29
$(OUT)/Pure: Pure
kleing@13301
    30
wenzelm@27203
    31
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
wenzelm@16019
    32
  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
wenzelm@44121
    33
  $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML		\
wenzelm@44121
    34
  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
wenzelm@44121
    35
  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
wenzelm@30160
    36
  $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
wenzelm@27203
    37
  $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
wenzelm@30165
    38
  $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
wenzelm@30165
    39
  $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
wenzelm@42793
    40
  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
wenzelm@42799
    41
  document/root.tex fologic.ML intprover.ML simpdata.ML
wenzelm@28500
    42
	@$(ISABELLE_TOOL) 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@27203
    49
$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
wenzelm@40239
    50
  ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy			\
ballarin@37134
    51
  ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy	\
ballarin@37134
    52
  ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy	\
wenzelm@40239
    53
  ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
wenzelm@40239
    54
  ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
wenzelm@40239
    55
  ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\
wenzelm@40239
    56
  ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
wenzelm@28500
    57
	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
wenzelm@2433
    58
wenzelm@4518
    59
wenzelm@4518
    60
## clean
wenzelm@4447
    61
wenzelm@4447
    62
clean:
wenzelm@27203
    63
	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz