nominal2: Quot/ROOT.ML@38aa6b67a80b (annotated)

604 0cf166548856 isabelle make tests all examples Christian Urban <urbanc@in.tum.de> parents: 601 diff changeset	1	quick_and_dirty := true;
0cf166548856 isabelle make tests all examples Christian Urban <urbanc@in.tum.de> parents: 601 diff changeset	2
0cf166548856 isabelle make tests all examples Christian Urban <urbanc@in.tum.de> parents: 601 diff changeset	3	no_document use_thys
601 81f40b8bde7b added "end" to each example theory Christian Urban <urbanc@in.tum.de> parents: 597 diff changeset	4	["QuotMain",
81f40b8bde7b added "end" to each example theory Christian Urban <urbanc@in.tum.de> parents: 597 diff changeset	5	"Examples/Fset",
81f40b8bde7b added "end" to each example theory Christian Urban <urbanc@in.tum.de> parents: 597 diff changeset	6	"Examples/IntEx",
81f40b8bde7b added "end" to each example theory Christian Urban <urbanc@in.tum.de> parents: 597 diff changeset	7	"Examples/IntEx2",
81f40b8bde7b added "end" to each example theory Christian Urban <urbanc@in.tum.de> parents: 597 diff changeset	8	"Examples/LFex",
81f40b8bde7b added "end" to each example theory Christian Urban <urbanc@in.tum.de> parents: 597 diff changeset	9	"Examples/LamEx"];

author	Christian Urban <urbanc@in.tum.de>
	Mon, 07 Dec 2009 18:49:14 +0100 (2009-12-07)
changeset 606	38aa6b67a80b
parent 604	0cf166548856
child 628	a11b9b757f89
permissions	-rw-r--r--