# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1331739714 0
# Node ID 39c387e690aa96e3a2d870e2c52aff7b8cb7fc28
# Parent  87eca760dcba0b2d35548d51504def4ff0536f9d
added ROOT.ML for tutorial

diff -r 87eca760dcba -r 39c387e690aa Tutorial/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/ROOT.ML	Wed Mar 14 15:41:54 2012 +0000
@@ -0,0 +1,19 @@
+
+quick_and_dirty := true;
+
+no_document use_thys
+   ["Lambda",
+    "Minimal",
+    "Tutorial1s",
+    "Tutorial3s",
+    "Tutorial4s",
+    "Tutorial1",
+    "Tutorial2",
+    "Tutorial2s",
+    "Tutorial3",
+    "Tutorial4",
+    "Tutorial5",
+    "Tutorial6" 
+   ];
+
+