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