# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360130281 0
# Node ID ba63ba7d282b6d3d2159845f67d79f960dd1e96d
# Parent  f47f1ef313d105ace9df79332e9e529e2952f1d3
updated

diff -r f47f1ef313d1 -r ba63ba7d282b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 06 05:49:16 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 05:58:01 2013 +0000
@@ -1345,7 +1345,7 @@
   but not with chap 3. For example:
   
   \begin{center}
-  @{term "[(L, 0), (L, 2), (R, 2), (R, 0)]"}
+  @{term "[(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
   \end{center}
 
   If started with @{term "([], [Oc])"} it halts with the
diff -r f47f1ef313d1 -r ba63ba7d282b paper.pdf
Binary file paper.pdf has changed