Formalisation of Turing Machines and Computability Theory
=========================================================

thys    - contains the formalisation

   Turing.thy:       Basic definitions of Turing machines.
   Turing_Hoare.thy: Contains the Hoare rules	
   Uncomputable.thy: The existence of Turing uncomputable functions
   Abacus_Mopup.thy: Mopup TM which is used when compiling Abacus
                     programs
   Abacus.thy:       Basic definitions of abacus machines (an intermediate
                     "language" for compiling recursive functions into 
                     Turing machines)
   Rec_Def.thy:      Basic definitions of recursive functions.
   Recursive.thy:    The compilation of recursive functions into
		     abacus machines.
   UF.thy:           The construction of the Universal Function, named "rec_F" and
                     the proof of its correctness.
   UTM.thy:          Obtaining a Universal Turing machine by translating the
                     Turing machine compiled from "rec_F" with some 
	             

Paper   - contains the files for the paper

Attic      - old files
Literature - related work


isabelle build -d . UTM
isabelle make utm     -- creates the big session file

isabelle make itp     -- creates paper



============================
ROOT setup

isabelle build -d . Slides2