regexp: IsaMakefile@288637d9dcde (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
334 d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	4	default: slides4
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	5	all: slides itp
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
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	17	## Slides 1
16 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
203 5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	22	@$(USEDIR) -D generated -f ROOT.ML HOL Slides
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	23
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	24	slides1: session1
24 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
367 79401279ba21 for slides urbanc parents: 334 diff changeset	27	cp Slides/generated/root.beamer.pdf Slides/slides1.pdf
24 f72c82bf59e5 added paper urbanc parents: 16 diff changeset	28
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	29	## Slides 2
203 5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	30
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	31	session2: Slides/ROOT.ML \
203 5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	32	Slides/document/root* \
5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	33	Slides/Slides1.thy
5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	34	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	35
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	36	slides2: session2
203 5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	37	rm -f Slides/generated/*.aux # otherwise latex will fall over
5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	38	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
367 79401279ba21 for slides urbanc parents: 334 diff changeset	39	cp Slides/generated/root.beamer.pdf Slides/slides2.pdf
203 5d724fe0e096 changes according to afp-submission urbanc parents: 162 diff changeset	40
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	41	## Slides 3
258 1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	42
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	43	session3: Slides/ROOT.ML \
258 1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	44	Slides/document/root* \
1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	45	Slides/Slides2.thy
1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	46	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides
1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	47
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	48	slides3: session3
258 1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	49	rm -f Slides/generated/*.aux # otherwise latex will fall over
1abf8586ee6b added slides for a talk in St Andrews urbanc parents: 203 diff changeset	50	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
367 79401279ba21 for slides urbanc parents: 334 diff changeset	51	cp Slides/generated/root.beamer.pdf Slides/slides3.pdf
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	52
334 d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	53	## Slides 4
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	54
334 d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	55	session4: Slides/ROOT.ML \
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	56	Slides/document/root* \
367 79401279ba21 for slides urbanc parents: 334 diff changeset	57	Slides/Slides4.thy
334 d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	58	@$(USEDIR) -D generated -f ROOT4.ML HOL Slides
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	59
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	60	slides4: session4
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	61	rm -f Slides/generated/*.aux # otherwise latex will fall over
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	62	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	63	cp Slides/generated/root.beamer.pdf Slides/slides4.pdf
72 e5116c2e6187 added an option fullpaper to IsaMakefile urbanc parents: 66 diff changeset	64
367 79401279ba21 for slides urbanc parents: 334 diff changeset	65	## Slides 5
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	66
367 79401279ba21 for slides urbanc parents: 334 diff changeset	67	session5: Slides/ROOT.ML \
79401279ba21 for slides urbanc parents: 334 diff changeset	68	Slides/document/root* \
79401279ba21 for slides urbanc parents: 334 diff changeset	69	Slides/Slides5.thy
79401279ba21 for slides urbanc parents: 334 diff changeset	70	@$(USEDIR) -D generated -f ROOT5.ML HOL Slides
79401279ba21 for slides urbanc parents: 334 diff changeset	71
79401279ba21 for slides urbanc parents: 334 diff changeset	72	slides5: session5
79401279ba21 for slides urbanc parents: 334 diff changeset	73	rm -f Slides/generated/*.aux # otherwise latex will fall over
79401279ba21 for slides urbanc parents: 334 diff changeset	74	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
79401279ba21 for slides urbanc parents: 334 diff changeset	75	cp Slides/generated/root.beamer.pdf Slides/slides5.pdf
79401279ba21 for slides urbanc parents: 334 diff changeset	76
79401279ba21 for slides urbanc parents: 334 diff changeset	77
79401279ba21 for slides urbanc parents: 334 diff changeset	78
79401279ba21 for slides urbanc parents: 334 diff changeset	79	slides: slides1 slides2 slides3 slides4 slides5
334 d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	80
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	81
d47c2143ab8a partially updated conference paper; slightly tuned journal paper urbanc parents: 333 diff changeset	82	## ITP itp
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	83
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	84	session_itp: Paper/ROOT.ML \
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	85	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	86	Paper/*.thy
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	87	@$(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	88
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	89	itp: session_itp
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	90	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	91	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
66 828ea293b61f more on the introduction urbanc parents: 62 diff changeset	92	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	93	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	94	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	95
162 e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	96	## Journal Version
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	97
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	98	session_journal: Journal/ROOT.ML \
162 e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	99	Journal/document/root* \
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	100	Journal/*.thy
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	101	@$(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	102
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	103	journal: session_journal
162 e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	104	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	105	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	106	cd Journal/generated ; bibtex root
e93760534354 added directory for journal version; took uptodate version of the theory files urbanc parents: 72 diff changeset	107	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	108	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	109
36 f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP wu parents: 31 diff changeset	110
16 663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	111	## clean
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	112
663816814e3e added initial slides for informal talk in Cambridge urbanc parents: diff changeset	113	clean:
333 813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	114	rm -rf Slides/generated*
813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	115	rm -rf Paper/generated*
813e7257c7c3 some polishing of the repository urbanc parents: 258 diff changeset	116	rm -rf Journal/generated*

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sat, 14 Sep 2013 14:08:19 +0100
changeset 387	288637d9dcde
parent 367	79401279ba21
permissions	-rw-r--r--