# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1357803248 0
# Node ID c5e3007fed2a3f060b161b714676acec80164436
# Parent  ae3d568b887b57d55a48838f465efe71ce0fa0ea
update

diff -r ae3d568b887b -r c5e3007fed2a Paper.thy
--- a/Paper.thy	Thu Jan 10 07:33:51 2013 +0000
+++ b/Paper.thy	Thu Jan 10 07:34:08 2013 +0000
@@ -257,7 +257,7 @@
 
   \noindent
   The first two clauses replace the head of the right-list
-  with new @{term Bk} or @{term Oc}, repsectively. To see that
+  with new a @{term Bk} or @{term Oc}, repsectively. To see that
   these clauses make sense in case where @{text r} is the empty
   list, one has to know that the tail function, @{term tl}, is defined
   such that @{term "tl [] == []"} holds. The third clause