diff -r f512026d5d6e -r 1abf8586ee6b Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Nov 11 23:38:10 2011 +0000
+++ b/Journal/Paper.thy	Sun Nov 20 22:53:50 2011 +0000
@@ -413,7 +413,7 @@
   \end{dfntn}
   
   \noindent
-  And then `forget' automata.
+  And then `forget' automata completely.
   The reason is that regular expressions, unlike graphs, matrices and
   functions, can be easily defined as an inductive datatype. A reasoning
   infrastructure (like induction and recursion) comes for free in
@@ -2114,9 +2114,9 @@
   @{term "Deriv_lang B A"} is regular.
 
   Even more surprising is the fact that for \emph{every} language @{text A}, the language
-  consisting of all substrings of @{text A} is regular \cite{Haines69} (see also 
+  consisting of all (scattered) substrings of @{text A} is regular \cite{Haines69} (see also 
   \cite{Shallit08, Gasarch09}). 
-  A \emph{substring} can be obtained
+  A \emph{(scattered) substring} can be obtained
   by striking out zero or more characters from a string. This can be defined 
   inductively in Isabelle/HOL by the following three rules: