(*
	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",
          "thys/UF"*)]