src/FOL/IsaMakefile
author oheimb
Thu May 15 15:51:09 1997 +0200 (1997-05-15 ago)
changeset 3206 a3de7f32728c
parent 3118 24dae6222579
child 3233 16a24111ab5a
permissions -rw-r--r--
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
     1 #
     2 # $Id$
     3 #
     4 # IsaMakefile for FOL
     5 #
     6 
     7 OUT = $(ISABELLE_OUTPUT)
     8 
     9 FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    10 	thy_data.ML cladata.ML \
    11 	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
    12 	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
    13 
    14 EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
    15 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
    16 	   ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    17 
    18 
    19 $(OUT)/FOL: $(OUT)/Pure $(FILES)
    20 	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
    21 	@chmod -w $@
    22 
    23 $(OUT)/Pure:
    24 	@cd ../Pure; $(ISATOOL) make
    25 
    26 test: ex/ROOT.ML $(OUT)/FOL $(EX_FILES)
    27 	@$(ISATOOL) usedir $(OUT)/FOL ex
    28 
    29 .PRECIOUS: $(OUT)/Pure $(OUT)/FOL