# HG changeset patch
# User urbanc
# Date 1298195664 0
# Node ID c7fdc28b8a76a578d4ae4eb0788f7b4264516138
# Parent  62925473bf6be19260214085c407a1283c980a69
latest update

diff -r 62925473bf6b -r c7fdc28b8a76 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 08:12:13 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 09:54:24 2011 +0000
@@ -1041,7 +1041,7 @@
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
   Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways how this string
-  is `split'  over @{term "A ;; B"}:
+  can be `distributed'  over @{term "A ;; B"}:
 
   \begin{center}
   \scalebox{0.7}{
@@ -1102,7 +1102,7 @@
   \noindent
   Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
   or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
-  In bot cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
+  In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
   following tagging-function
 
   \begin{center}