--- 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}