
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 




