regexp: IsaMakefile@e4d0e6cdc3d2 (annotated)

16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	1
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	2	## targets
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	3
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	4	default: paper
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	5	all: slides paper
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	6
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	7	## global settings
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	8
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	9	SRC = $(ISABELLE_HOME)/src
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	10	OUT = $(ISABELLE_OUTPUT)
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	11	LOG = $(OUT)/log
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	12
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	13
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	14	USEDIR = $(ISABELLE_TOOL) usedir -v true -t true
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	15
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	16
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	17	## Slides
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	18
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	19	session1: Slides/ROOT.ML \
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	20	Slides/document/root* \
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	21	Slides/Slides.thy
30 f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	22	@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	23
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	24	slides: session1
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	25	rm -f Slides/generated/*.aux # otherwise latex will fall over
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	26	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	27	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	28
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	29
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	30	## long paper
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	31
30 f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	32	session2: tphols-2011/ROOT.ML \
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	33	tphols-2011/document/root* \
31 b6815473ee2e 1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML zhang parents: 30 diff changeset	34	*.thy
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	35	@$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	36
f72c82bf59e5 added paper urbanc parents: 16 diff changeset	37	paper: session2
30 f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	38	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	39	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	40	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
30 f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	41	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	42
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	43
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	44	## ITP paper
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	45
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	46	session3: Paper/ROOT.ML \
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	47	Paper/document/root* \
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	48	Paper/*.thy
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	49	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	50
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	51	itp: session3
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	52	rm -f Paper/generated/*.aux # otherwise latex will fall over
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	53	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	54	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	55	cp Paper/generated/root.pdf paper.pdf
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	56
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	57
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	58	## clean
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	59
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	60	clean:
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	61	rm -rf Slides/generated/*
30 f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy]. zhang parents: 24 diff changeset	62	rm -rf tphols-2011/generated/*

author	wu
	Wed, 26 Jan 2011 22:58:24 +0000
changeset 37	e4d0e6cdc3d2
parent 36	f5cc33a0ba99
child 55	d71424eb5d0c
permissions	-rw-r--r--