diff -r 6746f5e1f1f8 -r 12772d537b71 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Fri Aug 18 14:51:29 2017 +0100
+++ b/thys/Paper/Paper.thy	Fri Aug 25 15:05:20 2017 +0200
@@ -143,7 +143,7 @@
 YES/NO answer for whether a string is being matched by a regular
 expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher
 to allow generation not just of a YES/NO answer but of an actual
-matching, called a [lexical] {\em value}. They give a simple algorithm
+matching, called a [lexical] {\em value}. \marginpar{explain what values are} They give a simple algorithm
 to calculate a value that appears to be the value associated with
 POSIX matching.  The challenge then is to specify that value, in an
 algorithm-independent fashion, and to show that Sulzmann and Lu's