diff -r 25b7d6bfd294 -r d688a01b8f89 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Tue Aug 21 14:14:19 2018 +0100
+++ b/thys/Journal/Paper.thy	Mon Sep 10 21:41:54 2018 +0100
@@ -1355,7 +1355,7 @@
   regular expression @{text r} and string @{term s} is in fact a
   minimal element of the values in @{text "LV r s"}. By
   Proposition~\ref{ordlen}\textit{(2)} we also know that any value in
-  @{text "LV s' r"}, with @{term "s'"} being a strict prefix, cannot be
+  @{text "LV r s'"}, with @{term "s'"} being a strict prefix, cannot be
   smaller than @{text "v\<^sub>1"}. The next theorem shows the
   opposite---namely any minimal element in @{term "LV r s"} must be a
   @{text POSIX} value. This can be established by induction on @{text