--- a/ROOT.ML	Thu Feb 07 06:39:06 2013 +0000
+++ b/ROOT.ML	Sun Feb 10 19:49:07 2013 +0000
@@ -1,22 +1,10 @@
-(*
-	turing_basic.thy : The basic definitions of Turing Machine.
-	uncomputable.thy : The existence of Turing uncomputable functions.
-	abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and
-	             the compilation of Abacus machines into Turing Machines.
-	rec_def.thy: The basic definitions of Recursive Functions.
-	recursive.thy : The compilation of Recursive Functions into
-		     Abacus machines.
-	UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness.
-	UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some 
-	         initialization and termination processing Turing Machines.
-*)
-  
+ 
 no_document 
-use_thys ["thys/turing_basic",
-          "thys/turing_hoare", 
-	  "thys/uncomputable", 
-	  "thys/abacus", 
-	  "thys/rec_def", 
-	  "thys/recursive",
+use_thys ["thys/Turing",
+          "thys/Turing_Hoare", 
+	  "thys/Uncomputable", 
+	  "thys/Abacus", 
+	  "thys/Rec_Def", 
+	  "thys/Recursive",
           "thys/UF",
           "thys/UTM"]