src/CCL/IsaMakefile
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 6213 f5bdd6497e08
child 13300 debf9ef73e4e
permissions -rw-r--r--
added HOL/Prolog
wenzelm@2489
     1
#
wenzelm@2489
     2
# $Id$
wenzelm@2489
     3
#
wenzelm@2489
     4
# IsaMakefile for CCL
wenzelm@2489
     5
#
wenzelm@2489
     6
wenzelm@4518
     7
## targets
wenzelm@4518
     8
wenzelm@4518
     9
default: CCL
wenzelm@4518
    10
images: CCL
wenzelm@4518
    11
test: CCL-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@2489
    20
wenzelm@4518
    21
wenzelm@4518
    22
## CCL
wenzelm@4518
    23
wenzelm@4518
    24
CCL: FOL $(OUT)/CCL
wenzelm@2489
    25
wenzelm@4518
    26
FOL:
wenzelm@4518
    27
	@cd $(SRC)/FOL; $(ISATOOL) make FOL
wenzelm@2489
    28
wenzelm@4518
    29
$(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \
wenzelm@4518
    30
  Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \
wenzelm@4518
    31
  Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \
wenzelm@4518
    32
  coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \
wenzelm@4518
    33
  typecheck.ML
wenzelm@6213
    34
	@$(ISATOOL) usedir -b -r $(OUT)/FOL CCL
wenzelm@2489
    35
wenzelm@4518
    36
wenzelm@4518
    37
## CCL-ex
wenzelm@2489
    38
wenzelm@4518
    39
CCL-ex: CCL $(LOG)/CCL-ex.gz
wenzelm@4518
    40
wenzelm@4518
    41
$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \
wenzelm@4518
    42
  ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy
wenzelm@2821
    43
	@$(ISATOOL) usedir $(OUT)/CCL ex
wenzelm@2489
    44
wenzelm@4518
    45
wenzelm@4518
    46
## clean
wenzelm@4447
    47
wenzelm@4447
    48
clean:
wenzelm@4518
    49
	@rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz