src/FOLP/IsaMakefile
author paulson
Mon Apr 26 13:25:49 1999 +0200 (1999-04-26)
changeset 6509 9f7f4fd05b1f
parent 4518 74c01296e818
child 17480 fd19f77dcf60
permissions -rw-r--r--
fixed a bug many years old in rule plusEC
wenzelm@2490
     1
#
wenzelm@2490
     2
# $Id$
wenzelm@2490
     3
#
wenzelm@2490
     4
# IsaMakefile for FOLP
wenzelm@2490
     5
#
wenzelm@2490
     6
wenzelm@4518
     7
## targets
wenzelm@4518
     8
wenzelm@4518
     9
default: FOLP
wenzelm@4518
    10
images: FOLP
wenzelm@4518
    11
test: FOLP-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@2490
    20
wenzelm@4518
    21
wenzelm@4518
    22
## FOLP
wenzelm@4518
    23
wenzelm@4518
    24
FOLP: Pure $(OUT)/FOLP
wenzelm@2490
    25
wenzelm@4518
    26
Pure:
wenzelm@4518
    27
	@cd $(SRC)/Pure; $(ISATOOL) make Pure
wenzelm@2490
    28
wenzelm@4518
    29
$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
wenzelm@4518
    30
  classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
wenzelm@2823
    31
	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
wenzelm@2490
    32
wenzelm@4518
    33
wenzelm@4518
    34
## FOLP-ex
wenzelm@2490
    35
wenzelm@4518
    36
FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
wenzelm@4518
    37
wenzelm@4518
    38
$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \
wenzelm@4518
    39
  ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \
wenzelm@4518
    40
  ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
wenzelm@2823
    41
	@$(ISATOOL) usedir $(OUT)/FOLP ex
wenzelm@2490
    42
wenzelm@4518
    43
wenzelm@4518
    44
## clean
wenzelm@4447
    45
wenzelm@4447
    46
clean:
wenzelm@4518
    47
	@rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz