nominal2: IsaMakefile@3e9b4ce0aeca (annotated)

1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	## targets
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
2440 0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2351 diff changeset	4	default: test
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	images:
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	7	all: tests paper pearl pearl-jv qpaper
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	8
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	## global settings
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	11
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	SRC = $(ISABELLE_HOME)/src
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	OUT = $(ISABELLE_OUTPUT)
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	LOG = $(OUT)/log
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ##-D generated
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	## Nominal2
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	21	tests: $(LOG)/HOL-Nominal2.gz
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
2480 ac7dff1194e8 introduced a general procedure for structural inductions; simplified reflexivity proof Christian Urban <urbanc@in.tum.de> parents: 2479 diff changeset	23	$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
ac7dff1194e8 introduced a general procedure for structural inductions; simplified reflexivity proof Christian Urban <urbanc@in.tum.de> parents: 2479 diff changeset	24	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	26	## Nominal2 Paper
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	27
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	paper: $(LOG)/HOL-Nominal2-Paper.gz
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
1775 86122d793f32 typos in paper Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	30	$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
2519 3e9b4ce0aeca added apendix to paper detailing one proof Christian Urban <urbanc@in.tum.de> parents: 2480 diff changeset	31	@$(USEDIR) -f ROOTa.ML -D generated HOL Paper
2479 a9b6a00b1ba0 updated to Isabelle Sept 16 Christian Urban <urbanc@in.tum.de> parents: 2459 diff changeset	32	@$(USEDIR) -D generated HOL Paper
1484 dc7b049d9072 made paper to compile Christian Urban <urbanc@in.tum.de> parents: 1261 diff changeset	33	$(ISABELLE_TOOL) document -o pdf Paper/generated
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	@cp Paper/document.pdf paper.pdf
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	35
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	36	## Pearl Paper ITP
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	37
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	38	pearl: $(LOG)/HOL-Pearl.gz
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	39
1775 86122d793f32 typos in paper Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	40	$(LOG)/HOL-Pearl.gz: Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	41	@$(USEDIR) -D generated HOL Pearl
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	42	$(ISABELLE_TOOL) document -o pdf Pearl/generated
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	43	@cp Pearl/document.pdf pearl.pdf
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	44
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	45	## Pearl Journal Paper
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	46
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	47	pearl-jv: $(LOG)/HOL-Pearl-jv.gz
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	48
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	49	$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Pearl-jv/document/root.* Pearl-jv/*.thy
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	50	@$(USEDIR) -D generated HOL Pearl-jv
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	51	$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	52	@cp Pearl-jv/document.pdf pearl-jv.pdf
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	53
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	54
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	55	## Quotient Paper
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	56
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	57	qpaper: $(LOG)/HOL-QPaper.gz
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	58
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	59	$(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	60	@$(USEDIR) -D generated HOL Quotient-Paper
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	61	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	62	@cp Quotient-Paper/document.pdf qpaper.pdf
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	63
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	64	## Slides
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	65
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	66	session1: Slides/ROOT1.ML \
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	67	Slides/document/root* \
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	68	Slides/Slides1.thy
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	69	@$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	70
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	71	slides1: session1
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	72	rm -f Slides/generated1/*.aux # otherwise latex will fall over
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	73	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	74	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	75	cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	76
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	77	session2: Slides/ROOT2.ML \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	78	Slides/document/root* \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	79	Slides/Slides2.thy
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	80	@$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	81
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	82	slides2: session2
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	83	rm -f Slides/generated2/*.aux # otherwise latex will fall over
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	84	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	85	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	86	cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	87
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	88	session3: Slides/ROOT3.ML \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	89	Slides/document/root* \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	90	Slides/Slides3.thy
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	91	@$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	92
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	93	slides3: session3
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	94	rm -f Slides/generated3/*.aux # otherwise latex will fall over
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	95	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	96	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	97	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	98
2459 ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	99	session4: Slides/ROOT4.ML \
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	100	Slides/document/root* \
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	101	Slides/Slides4.thy
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	102	@$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	103
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	104	slides4: session4
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	105	rm -f Slides/generated4/*.aux # otherwise latex will fall over
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	106	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	107	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	108	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	109
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	110	slides: slides4
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	111
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	112
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	113
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	114
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	## clean
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	116
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	clean:
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	118	@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz

author	Christian Urban <urbanc@in.tum.de>
	Fri, 08 Oct 2010 23:49:18 +0100
changeset 2519	3e9b4ce0aeca
parent 2480	ac7dff1194e8
child 2524	693562f03eee
permissions	-rw-r--r--