src/FOLP/IsaMakefile
author wenzelm
Tue Mar 18 22:19:18 2008 +0100 (2008-03-18 ago)
changeset 26322 eaf634e975fa
parent 25991 31b38a39e589
child 26408 6964c4799f47
permissions -rw-r--r--
converted legacy ML scripts;
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@26322
    29
$(OUT)/FOLP: $(OUT)/Pure FOLP.thy 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@26322
    38
$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy \
wenzelm@26322
    39
  ex/If.thy ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy   \
wenzelm@26322
    40
  ex/Classical.thy					    \
wenzelm@4518
    41
  ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
wenzelm@2823
    42
	@$(ISATOOL) usedir $(OUT)/FOLP ex
wenzelm@2490
    43
wenzelm@4518
    44
wenzelm@4518
    45
## clean
wenzelm@4447
    46
wenzelm@4447
    47
clean:
wenzelm@4518
    48
	@rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz