doc-src/Locales/IsaMakefile
author huffman
Thu, 26 May 2005 02:23:27 +0200
changeset 16081 81a4b4a245b0
parent 14586 7b8d56b4ac60
child 16168 adb83939177f
permissions -rw-r--r--
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     1
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     2
## targets
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     3
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     4
default: Locales
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     5
images:
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
test: Locales
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     7
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     8
all: images test
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     9
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    10
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    11
## global settings
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    12
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    13
SRC = $(ISABELLE_HOME)/src
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    14
OUT = $(ISABELLE_OUTPUT)
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    15
LOG = $(OUT)/log
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    16
USEDIR = $(ISATOOL) usedir -i true -d "" -D generated
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    17
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    18
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    19
## Locales
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    20
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    21
Locales: $(LOG)/HOL-Locales.gz
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    22
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    23
HOL:
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
	@cd $(SRC)/HOL; $(ISATOOL) make HOL
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    26
$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    27
	@$(USEDIR) $(OUT)/HOL Locales
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    28
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    29
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    30
## clean
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    32
clean:
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    33
	@rm -f $(LOG)/HOL-Locales.gz