1 (*

     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 	rec_def.thy: The basic definitions of Recursive Functions.

     7 	recursive.thy : The compilation of Recursive Functions into

     8 		     Abacus machines.

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

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

    11 	         initialization and termination processing Turing Machines.

    12 *)

    13   

    15 use_thys ["thys/turing_basic",

     3 use_thys ["thys/Turing",

    16           "thys/turing_hoare", 

     4           "thys/Turing_Hoare", 

    17 	  "thys/uncomputable", 

     5 	  "thys/Uncomputable", 

    18 	  "thys/abacus", 

     6 	  "thys/Abacus", 

    19 	  "thys/rec_def", 

     7 	  "thys/Rec_Def", 

    20 	  "thys/recursive",

     8 	  "thys/Recursive",