nominal2: Tutorial/ROOT.ML@b2e1a7b83e05 (annotated)

3133 39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	1
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	quick_and_dirty := true;
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	3
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	no_document use_thys
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	["Lambda",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	"Minimal",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	"Tutorial1s",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	"Tutorial3s",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	"Tutorial4s",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	"Tutorial1",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	"Tutorial2",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	"Tutorial2s",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	"Tutorial3",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	"Tutorial4",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	"Tutorial5",
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	"Tutorial6"
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	];
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
39c387e690aa added ROOT.ML for tutorial Christian Urban <urbanc@in.tum.de> parents: diff changeset	19

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 08 Jul 2014 11:18:31 +0100
changeset 3238	b2e1a7b83e05
parent 3133	39c387e690aa
permissions	-rw-r--r--