# HG changeset patch
# User urbanc
# Date 1298735078 0
# Node ID f1fea2c2713f0f912057bf6fbc51702023191e62
# Parent  cf95256005fe3d4036c270cac65d3563d11f9957
changed one occurence of tagging function into tagging relation

diff -r cf95256005fe -r f1fea2c2713f Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Feb 25 12:41:35 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 26 15:44:38 2011 +0000
@@ -1001,7 +1001,7 @@
   %
   \noindent
   since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
-  \eqref{pattern} we just have to unfold the definition of the tagging-relation and analyse 
+  \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse 
   in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. 
   The definition of the tagging-function will give us in each case the
   information to infer that @{text "y @ z \<in> A \<union> B"}.
@@ -1042,7 +1042,7 @@
   \end{center}
   %
   \noindent
-  where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
+  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 of how to `split' 
   this string to be in @{term "A ;; B"}:
@@ -1104,7 +1104,7 @@
   \end{center}
   %
   \noindent
-  Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
+  Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B},
   or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
   In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
   following tagging-function