diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Sun May 08 09:49:21 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 09 12:09:56 2016 +0100
@@ -62,6 +62,29 @@
 definition 
   "match r s \<equiv> nullable (ders s r)"
 
+(*
+comments not implemented
+
+p9. "None is returned, indicating an error is raised" : there is no error
+
+p9. The condtion "not exists s3 s4..." appears often enough (in particular in
+the proof of Lemma 3) to warrant a definition.
+
+p9. "The POSIX value v" : at this point the existence of a POSIX value is yet
+to be shown
+
+p10. (proof Lemma 3) : separating the cases with description/itemize would greatly
+improve readability
+
+p11. Theorem 2(2) : Stressing the uniqueness is strange, given that it follows
+trivially from the fact that "lexer" is a function. Maybe state the existence of
+a unique POSIX value as corollary.
+
+p14. Proposition 3 is evidently false and Proposition 4 is a conjecture.
+I find it confusing that Propositions 1 and 2, which are proven facts, are also called propositions.
+
+*)
+
 (*>*)
 
 section {* Introduction *}
@@ -414,7 +437,7 @@
   can match the empty string. If yes, we call the function @{const mkeps}
   that produces a value @{term "v\<^sub>4"} for how @{term "r\<^sub>4"} can
   match the empty string (taking into account the POSIX constraints in case
-  there are several ways). This functions is defined by the clauses:
+  there are several ways). This function is defined by the clauses:
 
 \begin{figure}[t]
 \begin{center}
@@ -519,7 +542,7 @@
 
   \noindent Consider first the @{text "else"}-branch where the derivative is @{term
   "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore
-  be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand
+  be of the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand
   side in clause~(4) of @{term inj}. In the @{text "if"}-branch the derivative is an
   alternative, namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c
   r\<^sub>2)"}. This means we either have to consider a @{text Left}- or
@@ -559,7 +582,7 @@
 
   \begin{proof}
   Both properties are by routine inductions: the first one can, for example,
-  be proved by an induction over the definition of @{term derivatives}; the second by
+  be proved by induction over the definition of @{term derivatives}; the second by
   an induction on @{term r}. There are no interesting cases.\qed
   \end{proof}
 
@@ -684,7 +707,7 @@
   preserves POSIX values.
 
   \begin{lemma}\label{Posix2}
-  @{thm[mode=IfThen] Posix2_roy_version}
+  @{thm[mode=IfThen] Posix_injval}
   \end{lemma}
 
   \begin{proof}
@@ -722,7 +745,7 @@
   \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain
   @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. Putting this all together allows us to infer
   @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}. The case @{text "(c)"}
-  is similarly.
+  is similar.
 
   For @{text "(b)"} we know @{term "s \<in> der c r\<^sub>2 \<rightarrow> v\<^sub>1"} and 
   @{term "s\<^sub>1 @ s\<^sub>2 \<notin> L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former
@@ -760,8 +783,8 @@
   \end{proof}
 
   \noindent This concludes our correctness proof. Note that we have not
-  changed the algorithm of Sulzmann and Lu,\footnote{Any deviation we
-  introduced is harmless.} but introduced our own specification for what a
+  changed the algorithm of Sulzmann and Lu,\footnote{All deviations we
+  introduced are harmless.} but introduced our own specification for what a
   correct result---a POSIX value---should be. A strong point in favour of
   Sulzmann and Lu's algorithm is that it can be extended in various ways.
 
@@ -891,23 +914,23 @@
   \end{center}
 
   \noindent
-  In the second clause we first calculate the derivative @{text "r \\ c"}
+  In the second clause we first calculate the derivative @{term "der c r"}
   and then simplify the result. This gives us a simplified derivative
   @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer
   is then recursively called with the simplified derivative, but before
-  we inject the character @{term c} into value, we need to rectify
+  we inject the character @{term c} into the value, we need to rectify
   it (that is construct @{term "f\<^sub>r v"}). We can prove that
 
-  \begin{lemma}
+  \begin{theorem}
   @{thm slexer_correctness}
-  \end{lemma}
+  \end{theorem}
 
   \noindent
   holds but for lack of space refer the reader to our mechanisation for details.
 
 *}
 
-section {* The Correctness Argument by Sulzmmann and Lu\label{argu} *}
+section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}
 
 text {*
 %  \newcommand{\greedy}{\succcurlyeq_{gr}}