isabelle: doc-src/Locales/IsaMakefile@5f263e81e366 (annotated)

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
16168 adb83939177f Locales: new element constrains, parameter renaming with syntax, ballarin parents: 14586 diff changeset	16	USEDIR = $(ISATOOL) usedir -i true -d "" -H false -D generated
14586 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
16168 adb83939177f Locales: new element constrains, parameter renaming with syntax, ballarin parents: 14586 diff changeset	26	$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy Locales/document/root.tex Locales/document/root.bib
14586 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

author	haftmann
	Thu, 16 Jun 2005 10:21:36 +0200
changeset 16404	5f263e81e366
parent 16168	adb83939177f
child 17098	dd769bd4d056
permissions	-rw-r--r--