--- a/Paper.thy	Fri Jan 11 05:45:40 2013 +0000
+++ b/Paper.thy	Fri Jan 11 05:49:25 2013 +0000
@@ -150,7 +150,7 @@
 formalisation we need arbitrary functions. But the general ideas for
 how to do this are clear enough in \cite{Boolos87}. However, one
 aspect that is completely left out from the informal description in
-\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing
+\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
 machines are correct. We will introduce Hoare-style proof rules
 which help us with such correctness arguments of Turing machines.