added ROOT.ML for tutorial
authorChristian Urban <urbanc@in.tum.de>
Wed, 14 Mar 2012 15:41:54 +0000
changeset 3133 39c387e690aa
parent 3132 87eca760dcba
child 3134 301b74fcd614
added ROOT.ML for tutorial
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" 
+   ];
+
+