src/CTT/IsaMakefile
author paulson
Tue Nov 14 13:26:48 2000 +0100 (2000-11-14)
changeset 10467 e6e7205e9e91
parent 4518 74c01296e818
child 19761 5cd82054c2c6
permissions -rw-r--r--
x-symbol support for Pi, Sigma, -->, : (membership)
note that "lam" is displayed as TWO lambda-symbols
wenzelm@2491
     1
#
wenzelm@2491
     2
# $Id$
wenzelm@2491
     3
#
wenzelm@2491
     4
# IsaMakefile for CTT
wenzelm@2491
     5
#
wenzelm@2491
     6
wenzelm@4518
     7
## targets
wenzelm@4518
     8
wenzelm@4518
     9
default: CTT
wenzelm@4518
    10
images: CTT
wenzelm@4518
    11
test: CTT-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@2491
    20
wenzelm@4518
    21
wenzelm@4518
    22
## CTT
wenzelm@4518
    23
wenzelm@4518
    24
CTT: Pure $(OUT)/CTT
wenzelm@2491
    25
wenzelm@4518
    26
Pure:
wenzelm@4518
    27
	@cd $(SRC)/Pure; $(ISATOOL) make Pure
wenzelm@2491
    28
wenzelm@4518
    29
$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \
paulson@10467
    30
  Bool.ML Bool.thy CTT.ML CTT.thy Main.thy ROOT.ML rew.ML
wenzelm@2823
    31
	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
wenzelm@2491
    32
wenzelm@4518
    33
wenzelm@4518
    34
## CTT-ex
wenzelm@2491
    35
wenzelm@4518
    36
CTT-ex: CTT $(LOG)/CTT-ex.gz
wenzelm@4518
    37
wenzelm@4518
    38
$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/elim.ML ex/equal.ML \
wenzelm@4518
    39
  ex/synth.ML ex/typechk.ML
wenzelm@2823
    40
	@$(ISATOOL) usedir $(OUT)/CTT ex
wenzelm@2491
    41
wenzelm@4518
    42
wenzelm@4518
    43
## clean
wenzelm@4447
    44
wenzelm@4447
    45
clean:
wenzelm@4518
    46
	@rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz