regexp: IsaMakefile@d371536861bc (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
55 d71424eb5d0c Myhill.thy IsabelleMakefile modified zhang parents: 36 diff changeset	35	@$(USEDIR) -D generated -f ROOT.ML ListP 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
72 e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	43	## full paper
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	44
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	45	fullsession2: tphols-2011/ROOT.ML \
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	46	tphols-2011/document/root* \
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	47	*.thy
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	48	@$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	49
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	50	fullpaper: fullsession2
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	51	rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	52	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	53	cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	54	cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	55
e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	56
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	57
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	58	## ITP paper
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	59
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	60	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	61	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	62	Paper/*.thy
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	63	@$(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	64
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	65	itp: session3
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	66	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	67	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
66 828ea293b61f more on the introduction urbanc parents: 62 diff changeset	68	cd Paper/generated ; bibtex root
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	69	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	70	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	71
162 e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	72	## Journal Version
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	73
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	74	session4: Journal/ROOT.ML \
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	75	Journal/document/root* \
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	76	Journal/*.thy
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	77	@$(USEDIR) -D generated -f ROOT.ML HOL Journal
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	78
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	79	journal: session4
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	80	rm -f Journal/generated/*.aux # otherwise latex will fall over
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	81	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	82	cd Journal/generated ; bibtex root
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	83	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	84	cp Journal/generated/root.pdf journal.pdf
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	85
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	86
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	87	## clean
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	88
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	89	clean:
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	90	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	91	rm -rf tphols-2011/generated/*

author	urbanc
	Tue, 26 Jul 2011 10:58:26 +0000
changeset 173	d371536861bc
parent 162	e93760534354
child 203	5d724fe0e096
permissions	-rw-r--r--