--- a/Paper.thy	Sun Dec 30 21:18:39 2012 +0000
+++ b/Paper.thy	Sun Dec 30 22:15:54 2012 +0000
@@ -56,17 +56,24 @@
 
 
 
-
-\cite{AspertiRicciotti12}
+``In particular, the fact that the universal machine operates with a
+different alphabet with respect to the machines it simulates is
+annoying.'' he writes it is preliminary work \cite{AspertiRicciotti12}
 
 
-Our formalisation follows XXX
+Our formalisation follows \cite{Boolos87}
 
 \noindent
 {\bf Contributions:} 
 
 *}
 
+section {* Formalisation *}
+
+text {*
+
+*}
+
 
 section {* Wang Tiles *}