1 (*

     2 	turing_basic.thy : The basic definitions of Turing Machine.

     3 	uncomputable.thy : The existence of Turing uncomputable functions.

     4 	abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and

     5 	             the compilation of Abacus machines into Turing Machines.

     6 	recursive.thy : The basic defintions of Recursive Functions and the compilation of Recursive Functions into

     7 		     Abacus machines.

     8 	UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness.

     9 	UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some 

    10 	         initialization and termination processing Turing Machines.

    11 *)

    12   no_document use_thys ["turing_basic", "uncomputable", "abacus", "recursive", "UF", "UTM"]