diff -r fb201e383f1b -r da575186d492 Tutorial/ROOT.ML
--- a/Tutorial/ROOT.ML	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-
-quick_and_dirty := true;
-
-no_document use_thys
-   ["Lambda",
-    "Minimal",
-    "Tutorial1s",
-    "Tutorial3s",
-    "Tutorial4s",
-    "Tutorial1",
-    "Tutorial2",
-    "Tutorial2s",
-    "Tutorial3",
-    "Tutorial4",
-    "Tutorial5",
-    "Tutorial6" 
-   ];
-
-