# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1457434003 0
# Node ID fee5641c5994cf8bb3f30f7408b806610ddb6931
# Parent  2f043f8be9a9c64ebc20fa64d45f7fbb0ccf9723
updated

diff -r 2f043f8be9a9 -r fee5641c5994 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Mar 08 10:40:35 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 10:46:43 2016 +0000
@@ -527,7 +527,7 @@
   (STAR r)"}. Finally, the reason for why we can ignore the second argument
   in clause (1) of @{term inj} is that it will only ever be called in cases
   where @{term "c=d"}, but the usual linearity restrictions in patterns do
-  not allow is to build this constraint explicitly into our function
+  not allow us to build this constraint explicitly into our function
   definition.\footnote{Sulzmann and Lu state this clause as @{thm (lhs)
   injval.simps(1)[of "c" "c"]} $\dn$ @{thm (rhs) injval.simps(1)[of "c"]},
   but our deviation is harmless.}
@@ -638,16 +638,14 @@
   A similar condition is imposed on the POSIX value in the @{text
   "P\<star>"}-rule. Also there we want that @{term "s\<^sub>1"} is the longest initial
   split of @{term "s\<^sub>1 @ s\<^sub>2"} and furthermore the corresponding value
-  @{term v} cannot be flatten to the empty string. In effect, we require
+  @{term v} cannot be flattened to the empty string. In effect, we require
   that in each ``iteration'' of the star, some non-empty substring need to
   be ``chipped'' away; only in case of the empty string we accept @{term
   "Stars []"} as the POSIX value.
 
    We can prove that given a string @{term s} and regular expression @{term
    r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow>
-   v"} (albeilt in an uncomputable fashion---for example rule @{term "P+R"}
-   would require the calculation of the potentially infinite set @{term "L
-   r\<^sub>1"}).
+   v"}.
 
   \begin{theorem}
   @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
@@ -661,7 +659,7 @@
 
   \noindent
   Next is the lemma that shows the function @{term "mkeps"} calculates
-  the posix value for the empty string and a nullable regular expression.
+  the POSIX value for the empty string and a nullable regular expression.
 
   \begin{lemma}\label{lemmkeps}
   @{thm[mode=IfThen] PMatch_mkeps}
diff -r 2f043f8be9a9 -r fee5641c5994 thys/paper.pdf
Binary file thys/paper.pdf has changed