5 

     6    Turing.thy:       Basic definitions of Turing machines.

     7    Turing_Hoare.thy: Contains the Hoare rules	

     8    Uncomputable.thy: The existence of Turing uncomputable functions

     9    Abacus.thy:       Basic definitions of abacus machines (an intermediate

    10                      "language" for compiling recursive functions into 

    11                      Turing machines)

    12    Rec_Def.thy:      Basic definitions of recursive functions.

    13    Recursive.thy:    The compilation of recursive functions into

    14 		     abacus machines.

    15    UF.thy:           The construction of the Universal Function, named "rec_F" and

    16                      the proof of its correctness.

    17    UTM.thy:          Obtaining a Universal Turing machine by translating the

    18                      Turing machine compiled from "rec_F" with some 

    19 	             

    20