--- a/thys/Paper/Paper.thy	Sun Mar 06 12:48:31 2016 +0000
+++ b/thys/Paper/Paper.thy	Sun Mar 06 16:51:32 2016 +0000
@@ -464,7 +464,7 @@
 
   \begin{center}
   \begin{tabular}{lcl}
-  @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
+  @{thm (lhs) injval.simps(1)[of "d" "DUMMY"]} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
   @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
       @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
   @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
@@ -482,13 +482,30 @@
 
   \noindent To better understand what is going on in this definition it
   might be instructive to look first at the three sequence cases (clauses
-  4--6). Recall the corresponding clause of the derivative
+  4--6). In each case we need to construct an ``injected value'' for @{term
+  "SEQ r\<^sub>1 r\<^sub>2"}. Recall the clause of the @{const der}-function
+  for sequence regular expressions:
 
   \begin{center}
   @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}
   \end{center}
 
-  \noindent
+  \noindent Consider first the 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 fourth
+  clause of @{term inj}. In the 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 @{text
+  Right}-value. In case of the @{text Left}-value we know further it must be 
+  a value for a sequence regular expression. Therefore the pattern we
+  match in the fifth clause is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while
+  in the sixth it is just @{term "Right v\<^sub>2"}. One more interesting point
+  is in the right-hand side of the sixth clause: since in this case the regular
+  expression @{text "r\<^sub>1"} does not ``contribute'' in matching the string,
+  that is only matches the empty string, we need to call @{const mkeps} in order 
+  to construct a value how @{term "r\<^sub>1"} can match this empty string.
+
+
   NOT DONE YET 
 
   Therefore there are, for example, three