--- a/ROOT.ML	Mon Dec 24 01:26:23 2012 +0000
+++ b/ROOT.ML	Wed Dec 26 14:52:14 2012 +0000
@@ -10,4 +10,12 @@
 	UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some 
 	         initialization and termination processing Turing Machines.
 *)
-   use_thys ["turing_basic", "uncomputable", "abacus", "rec_def", "recursive", "UF", "UTM"]
+  
+no_document 
+use_thys ["turing_basic", 
+	  "uncomputable", 
+	  "abacus", 
+	  "rec_def", 
+	  "recursive", 
+	  "UF", 
+          "UTM"]