(* 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"]