nominal2: IsaMakefile@b577f06e0804 (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
2524 693562f03eee major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) Christian Urban <urbanc@in.tum.de> parents: 2519 diff changeset	4	default: tests
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
2748 6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	7	all: tests esop pearl pearl-jv qpaper slides
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
2749 7cf2d79d8d5e tuned IsaMakefile Christian Urban <urbanc@in.tum.de> parents: 2748 diff changeset	24	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal2
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
2748 6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	26	## ESOP Paper
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	27
2748 6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	28	esop: $(LOG)/HOL-ESOP-Paper.gz
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	29
2748 6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	30	$(LOG)/HOL-ESOP-Paper.gz: ESOP-Paper/ROOT.ML ESOP-Paper/document/root.* ESOP-Paper/*.thy
2749 7cf2d79d8d5e tuned IsaMakefile Christian Urban <urbanc@in.tum.de> parents: 2748 diff changeset	31	@$(USEDIR) -f ROOT.ML -D generated Nominal2 ESOP-Paper
2748 6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	32	$(ISABELLE_TOOL) document -o pdf ESOP-Paper/generated
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	33	@cp ESOP-Paper/document.pdf esop-paper.pdf
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	34
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	35	## Pearl Paper ITP
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	36
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	37	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	38
1775 86122d793f32 typos in paper Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	39	$(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	40	@$(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	41	$(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	42	@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	43
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	44	## Pearl Journal Paper
95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	45
2742 f1192e3474e0 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	46	$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Nominal/*.thy
f1192e3474e0 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	47	@cd Pearl-jv; $(USEDIR) -b -f ROOT.ML HOL HOL-Pearl-jv
1785 95df71c3df2f added new paper directory for further work Christian Urban <urbanc@in.tum.de> parents: 1775 diff changeset	48
2742 f1192e3474e0 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	49	pearl-jv: $(LOG)/HOL-Pearl-jv.gz Pearl-jv/ROOT2.ML Pearl-jv/document/root.* Pearl-jv/*.thy
f1192e3474e0 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	50	@$(USEDIR) -f ROOT2.ML -D generated HOL-Pearl-jv Pearl-jv
f1192e3474e0 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	51	@$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated
f1192e3474e0 more on the paper Christian Urban <urbanc@in.tum.de> parents: 2524 diff changeset	52	@cp Pearl-jv/document.pdf pearl-jv.pdf
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	53
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	54	## Quotient Paper
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	55
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	56	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	57
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	58	$(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	59	@$(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	60	$(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	61	@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	62
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	63	## Slides
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	64
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	65	session1: Slides/ROOT1.ML \
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	66	Slides/document/root* \
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	67	Slides/Slides1.thy
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	68	@$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	69
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	70	slides1: session1
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	71	rm -f Slides/generated1/*.aux # otherwise latex will fall over
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	72	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
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
2351 842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	74	cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	75
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	76	session2: Slides/ROOT2.ML \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	77	Slides/document/root* \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	78	Slides/Slides2.thy
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	79	@$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	80
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	81	slides2: session2
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	82	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	83	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	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	cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	86
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	87	session3: Slides/ROOT3.ML \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	88	Slides/document/root* \
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	89	Slides/Slides3.thy
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	90	@$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	91
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	92	slides3: session3
842969a598f2 added material for slides Christian Urban <urbanc@in.tum.de> parents: 2299 diff changeset	93	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	94	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	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	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	97
2459 ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	98	session4: Slides/ROOT4.ML \
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	99	Slides/document/root* \
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	100	Slides/Slides4.thy
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	101	@$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	102
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	103	slides4: session4
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	104	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	105	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	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	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf
ac3470e1e5af slides of my talk Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	108
2748 6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	109	session5: Slides/ROOT5.ML \
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	110	Slides/document/root* \
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	111	Slides/Slides5.thy
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	112	@$(USEDIR) -D generated5 -f ROOT5.ML HOL-Nominal Slides
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	113
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	114	slides5: session5
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	115	rm -f Slides/generated5/*.aux # otherwise latex will fall over
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	116	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	117	cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	118	cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf
6f38e357b337 rearranged directories and updated to new Isabelle Christian Urban <urbanc@in.tum.de> parents: 2742 diff changeset	119
2762 1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	120	session6: Slides/ROOT6.ML \
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	121	Slides/document/root* \
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	122	Slides/Slides6.thy
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	123	@$(USEDIR) -D generated6 -f ROOT6.ML HOL-Nominal Slides
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	124
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	125	slides6: session6
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	126	rm -f Slides/generated6/*.aux # otherwise latex will fall over
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	127	cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	128	cd Slides/generated6 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	129	cp Slides/generated6/root.beamer.pdf Slides/slides6.pdf
1a1a2b778ba2 Shanghai slides Christian Urban <urbanc@in.tum.de> parents: 2749 diff changeset	130
2772 c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	131	session7: Slides/ROOT7.ML \
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	132	Slides/document/root* \
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	133	Slides/Slides6.thy
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	134	@$(USEDIR) -D generated7 -f ROOT7.ML HOL Slides
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	135
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	136	slides7: session7
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	137	rm -f Slides/generated7/*.aux # otherwise latex will fall over
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	138	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	139	cd Slides/generated7 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	140	cp Slides/generated7/root.beamer.pdf Slides/slides7.pdf
c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	141
2785 c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	142	session8: Slides/ROOT8.ML \
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	143	Slides/document/root* \
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	144	Slides/Slides6.thy
2786 bccda961a612 more on slides Christian Urban <urbanc@in.tum.de> parents: 2785 diff changeset	145	@$(USEDIR) -D generated8 -f ROOT8.ML HOL-Nominal Slides
2772 c3ff26204d2a added slides for beijing Christian Urban <urbanc@in.tum.de> parents: 2762 diff changeset	146
2785 c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	147	slides8: session8
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	148	rm -f Slides/generated8/*.aux # otherwise latex will fall over
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	149	cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	150	cd Slides/generated8 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	151	cp Slides/generated8/root.beamer.pdf Slides/slides8.pdf
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	152
c63ffe1735eb added slides for copenhagen Christian Urban <urbanc@in.tum.de> parents: 2772 diff changeset	153	slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8
2299 09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	154
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	155
09bbed4f21d6 added slides Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	156
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: 1785 diff changeset	157
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	158	## clean
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	159
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	160	clean:
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	161	@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Wed, 15 Jun 2011 11:06:31 +0900
changeset 2854	b577f06e0804
parent 2786	bccda961a612
child 2856	e36beb11723c
permissions	-rw-r--r--