Mention RegExp2NA.

--- a/src/HOL/Lex/README.html	Mon Aug 17 13:09:40 1998 +0200
+++ b/src/HOL/Lex/README.html	Mon Aug 17 16:02:21 1998 +0200
@@ -7,14 +7,18 @@
 This directory contains the theories for the functional scanner generator
 described
 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html">
-here</A>.
+here</A>. In contrast to the paper, the latest version of the theories
+provides a fully executable scanner generator. The non-executable bits
+(transitive closure) have been eliminated by going from regular expressions
+directly to nondeterministic automata, thus bypassing epsilon-moves.
+<br>
 <br>
 Overview:
 <dl>
 <dt>Automata</dt>
 <dd>AutoProj, NA, NAe, DA, Automata</dd>
 <dt>Regular expressions and their conversion to automata</dt>
-<dd>RegSet, RegExp, RegExp2NAe</dd>
+<dd>RegSet, RegExp, RegExp2NA, RegExp2NAe</dd>
 <dt>Scanning</dt>
 <dd>Prefix, MaxPrefix, MaxChop, AutoMaxChop, Scanner</dd>
 </dl>