isabelle-cookbook: ProgTutorial/Package/IsaMakefile@620a24bf954a (annotated)

205 f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	## targets
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	default: simple-keyword
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	images:
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	test: simple-keyword
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	7
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	all: images test
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	## global settings
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	SRC = $(ISABELLE_HOME)/src
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	OUT = $(ISABELLE_OUTPUT)
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	LOG = $(OUT)/log
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	16
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf ## -D generated
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	## simple-keyword
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	simple-keyword: $(LOG)/HOL-Nominal-simple-keyword.gz
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	23
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	$(LOG)/HOL-Nominal-simple-keyword.gz: ## simple-keyword/ROOT.ML simple-keyword/document/root.tex simple-keyword/*.thy
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	@$(USEDIR) HOL-Nominal simple-keyword
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	## clean
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	clean:
f8d4393d6fdd added infrastructure to generate the keyword file for simple_inductive Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	@rm -f $(LOG)/HOL-Nominal-simple-keyword.gz

author	Christian Urban <urbanc@in.tum.de>
	Sat, 24 Apr 2010 22:55:50 +0200
changeset 421	620a24bf954a
parent 205	f8d4393d6fdd
permissions	-rw-r--r--