4 thys    - contains the formalisation

     4 thys    - contains the formalisation

     5 

     5 

     6    Turing.thy:       Basic definitions of Turing machines.

     6    Turing.thy:       Basic definitions of Turing machines.

     7    Turing_Hoare.thy: Contains the Hoare rules	

     7    Turing_Hoare.thy: Contains the Hoare rules	

     8    Uncomputable.thy: The existence of Turing uncomputable functions

     8    Uncomputable.thy: The existence of Turing uncomputable functions

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

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

    10                      "language" for compiling recursive functions into 

    12                      "language" for compiling recursive functions into 

    11                      Turing machines)

    13                      Turing machines)

    12    Rec_Def.thy:      Basic definitions of recursive functions.

    14    Rec_Def.thy:      Basic definitions of recursive functions.

    13    Recursive.thy:    The compilation of recursive functions into

    15    Recursive.thy:    The compilation of recursive functions into