(*+ −
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 ["turing_basic", + −
"uncomputable", + −
"abacus", + −
"rec_def", + −
"recursive", + −
"UF", + −
"UTM"];+ −
+ −
+ −
use_thys ["Paper"]+ −