nominal2: Tutorial/ROOT.ML@a29b35442d1c (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	Cezary Kaliszyk <cezarykaliszyk@gmail.com>
	Fri, 20 Apr 2012 15:58:13 +0200 (2012-04-20)
changeset 3163	a29b35442d1c
parent 3133	39c387e690aa
permissions	-rw-r--r--