--- a/utm/ROOT.ML	Sat Sep 29 12:38:12 2012 +0000
+++ b/utm/ROOT.ML	Mon Oct 15 13:23:52 2012 +0000
@@ -3,10 +3,11 @@
 	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.
-	recursive.thy : The basic defintions of Recursive Functions and the compilation of Recursive Functions into
+	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", "recursive", "UF", "UTM"]
+   use_thys ["turing_basic", "uncomputable", "abacus", "rec_def", "recursive", "UF", "UTM"]