--- 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}