nominal2: Nominal/ROOT.ML@12283a96e851 (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
2330 8728f7990f6d merged cezary's changes Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	3	(*
1261 853abc14c5c6 added IsaMakefile...but so far included only a test for the parser Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	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	5	["Ex/Lambda",
2083 9568f9f31822 tuned file names for examples Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	6	"Ex/LF",
1911 60b5c61d3de2 renamed Ex1.thy to SingleLet.thy Christian Urban <urbanc@in.tum.de> parents: 1797 diff changeset	7	"Ex/SingleLet",
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	8	"Ex/Ex1rec",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	9	"Ex/Ex2",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	10	"Ex/Ex3",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	11	"Ex/ExLet",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	12	"Ex/ExLetRec",
1795 e39453c8b186 tuned type-schemes example Christian Urban <urbanc@in.tum.de> parents: 1774 diff changeset	13	"Ex/TypeSchemes",
2083 9568f9f31822 tuned file names for examples Christian Urban <urbanc@in.tum.de> parents: 2062 diff changeset	14	"Ex/Modules",
1773 c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	15	"Ex/ExPS3",
c0eac04ae3b4 added README and moved examples into separate directory Christian Urban <urbanc@in.tum.de> parents: 1656 diff changeset	16	"Ex/ExPS7",
2142 c39d4fe31100 moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat Christian Urban <urbanc@in.tum.de> parents: 2137 diff changeset	17	"Ex/CoreHaskell",
2288 3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2142 diff changeset	18	"Ex/Test"(*,
3b83960f9544 new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files Christian Urban <urbanc@in.tum.de> parents: 2142 diff changeset	19	"Manual/Term4"*)
1604 5ab97f43ec24 More modification needed for compilation Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1485 diff changeset	20	];
2330 8728f7990f6d merged cezary's changes Christian Urban <urbanc@in.tum.de> parents: 2288 diff changeset	21	*)

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Thu, 19 Aug 2010 15:46:28 +0900 (2010-08-19)
changeset 2416	12283a96e851
parent 2330	8728f7990f6d
child 2440	0a36825b16c1
permissions	-rw-r--r--