diff -r 692b62426677 -r deea42c83c9e thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/Journal/Paper.thy	Thu Oct 05 12:45:13 2017 +0100
@@ -223,10 +223,10 @@
 \noindent where @{const Stars}, @{text Left}, @{text Right} and @{text
 Char} are constructors for values. @{text Stars} records how many
 iterations were used; @{text Left}, respectively @{text Right}, which
-alternative is used. This `tree view' leads naturally to the
-idea that regular expressions act as types and values as inhabiting
-those types. This view was first put forward by ???. The value for the
-single `iteration', i.e.~the POSIX value, would look as follows
+alternative is used. This `tree view' leads naturally to the idea that
+regular expressions act as types and values as inhabiting those types
+(see, for example, \cite{HosoyaVouillonPierce2005}).  The value for
+the single `iteration', i.e.~the POSIX value, would look as follows
 
 \begin{center}
 @{term "Stars [Seq (Char x) (Char y)]"}
@@ -1253,8 +1253,8 @@
   being inhabited by the same regular expression. The
   complexity of the proofs involved seems to not justify such a
   `cleaner' single statement. The statements given are just the properties that
-  allow us to establish our theorems. The proofs for Proposition~\ref{ordintros}
-  are routine.
+  allow us to establish our theorems without any difficulty. The proofs 
+  for Proposition~\ref{ordintros} are routine.
  
 
   Next we establish how Okui and Suzuki's orderings relate to our