nominal2: Tutorial/ROOT.ML@da59c94bed7e (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 <urbanc@in.tum.de>
	Wed, 04 Apr 2012 06:19:38 +0100
changeset 3152	da59c94bed7e
parent 3133	39c387e690aa
permissions	-rw-r--r--