nominal2: Nominal/ROOT.ML@69780ae147f5 (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
2440 0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	2
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	no_document use_thys
2440 0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	4	["Ex/Classical",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	5	"Ex/CoreHaskell",
2482 0c2eb0ed30a0 fixed Christian Urban <urbanc@in.tum.de> parents: 2481 diff changeset	6	"Ex/Datatypes",
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	7	"Ex/Ex1",
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	8	"Ex/ExPS3",
2481 3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	9	"Ex/Multi_Recs",
3a5ebb2fcdbf made supp proofs more robust by not using the standard induction; renamed some example files Christian Urban <urbanc@in.tum.de> parents: 2454 diff changeset	10	"Ex/Multi_Recs2",
2440 0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	11	"Ex/LF",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	12	"Ex/Lambda",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	13	"Ex/Let",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	14	"Ex/LetPat",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	15	"Ex/LetRec",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	16	"Ex/LetRec2",
2454 9ffee4eb1ae1 renamed NewParser to Nominal2 Christian Urban <urbanc@in.tum.de> parents: 2440 diff changeset	17	"Ex/LetFun",
2440 0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	18	"Ex/Modules",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	19	"Ex/SingleLet",
0a36825b16c1 "isabelle make test" makes all major examples....they work up to supp theorems (excluding) Christian Urban <urbanc@in.tum.de> parents: 2330 diff changeset	20	"Ex/TypeSchemes",
2494 11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: 2482 diff changeset	21	"Ex/TypeVarsTest",
11133eb76f61 added Foo1 to explore a contrived example Christian Urban <urbanc@in.tum.de> parents: 2482 diff changeset	22	"Ex/Foo1"
1604 5ab97f43ec24 More modification needed for compilation Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1485 diff changeset	23	];

author	Christian Urban <urbanc@in.tum.de>
	Wed, 06 Oct 2010 21:32:44 +0100 (2010-10-06)
changeset 2514	69780ae147f5
parent 2494	11133eb76f61
child 2556	8ed62410236e
permissions	-rw-r--r--