latest update
authorurbanc
Sun, 20 Feb 2011 09:54:24 +0000
changeset 126 c7fdc28b8a76
parent 125 62925473bf6b
child 127 8440863a9900
latest update
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}