--- a/Paper.thy	Thu Jan 10 12:30:27 2013 +0000
+++ b/Paper.thy	Thu Jan 10 13:03:25 2013 +0000
@@ -334,9 +334,7 @@
   \end{tabular}
   \end{center}
 
-  start state
-
-  What is tinres? What is it used for?
+  start state 1 final state 0
 
   \begin{center}
   @{thm dither_def}