diff -r fe7a257bdff4 -r dfe852aacae6 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jan 30 03:33:05 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 03:46:22 2013 +0000
@@ -15,7 +15,7 @@
 consts DUMMY::'a
 
 notation (latex output)
-  Cons ("_::_" [78,77] 73) and
+  Cons ("_::_" [48,47] 48) and
   set ("") and
   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
@@ -899,7 +899,10 @@
   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
-  @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}
+  @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
+  @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
+                               &             & @{thm (rhs) inv_loop1_exit.simps}\\
+  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}\\
   \end{tabular}
   \end{center}
   \caption{The invariants for each state of @{term tcopy_begin}. They depend on