# HG changeset patch
# User nipkow
# Date 903362541 -7200
# Node ID 39a81cd9f9421164ec3a6170e8fd0c21668ef1e7
# Parent  8f9056ce5dfbd04ea1b175aa67376c215ab1c7d0
Mention RegExp2NA.

diff -r 8f9056ce5dfb -r 39a81cd9f942 src/HOL/Lex/README.html
--- 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>