nominal2: IsaMakefile@4b4742aa43f2 (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
3070 4b4742aa43f2 cleaned all papers from the stable branch Christian Urban <urbanc@in.tum.de> parents: 2996 diff changeset	7	all: tests
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
2996 aedcf9e5aa3b Add 'no-brackets' to avoid '[\| \|]' in papers. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 2985 diff changeset	16	USEDIR = $(ISABELLE_TOOL) usedir -v true -t true -m no_brackets ##-D generated
1261 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
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	## clean
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	clean:
1772 48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory Christian Urban <urbanc@in.tum.de> parents: 1491 diff changeset	29	@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz

author	Christian Urban <urbanc@in.tum.de>
	Sat, 17 Dec 2011 17:03:01 +0000 (2011-12-17)
branch	Nominal2-Isabelle2011-1
changeset 3070	4b4742aa43f2
parent 2996	aedcf9e5aa3b
permissions	-rw-r--r--