--- a/README	Thu Feb 07 06:39:06 2013 +0000
+++ b/README	Sun Feb 10 19:49:07 2013 +0000
@@ -1,9 +1,24 @@
-Formalisation of Turing Machines
-================================
+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.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