nominal2: Nominal/ROOT.ML@65bdcc42badd (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	quick_and_dirty := true;
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	2
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
1797 fddb470720f1 renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper Christian Urban <urbanc@in.tum.de> parents: 1795 diff changeset	4	["Ex/Lambda",
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	5	"Ex/ExLF",
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	6	"Ex/SingleLet",
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	7	"Ex/Ex1rec",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	8	"Ex/Ex2",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	9	"Ex/Ex3",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	10	"Ex/ExLet",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	11	"Ex/ExLetRec",
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	12	"Ex/TypeSchemes",
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	13	"Ex/ExLeroy",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	14	"Ex/ExPS3",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	15	"Ex/ExPS7",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	16	"Ex/ExCoreHaskell",
2062 65bdcc42badd "isabelle make" compiles all examples with newparser/newfv/newalpha only. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	17	"Ex/Test",
65bdcc42badd "isabelle make" compiles all examples with newparser/newfv/newalpha only. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1911 diff changeset	18	"Manual/Term4"
1604 5ab97f43ec24 More modification needed for compilation Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1485 diff changeset	19	];

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Tue, 04 May 2010 17:25:58 +0200 (2010-05-04)
changeset 2062	65bdcc42badd
parent 1911	60b5c61d3de2
child 2083	9568f9f31822
permissions	-rw-r--r--