--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ROOT1.ML	Wed Dec 26 19:03:06 2012 +0000
@@ -0,0 +1,24 @@
+(*
+	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 ["turing_basic", 
+          "uncomputable", 
+          "abacus", 
+          "rec_def", 
+          "recursive", 
+          "UF", 
+          "UTM"];
+
+
+use_thys ["Paper"]