--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/README.html	Sat Nov 18 14:55:44 1995 +0100
@@ -0,0 +1,41 @@
+<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
+<BODY>
+
+<H2>A Simplified Scanner Generator</H2>
+
+This is half of a simplified functional scanner generator. The overall design
+is like this:
+<PRE>
+         regular expression
+                  |
+                  v
+             -----------
+             | mk_auto |
+             -----------
+                  |
+        deterministic automaton
+                  |
+                  v
+           ----------------
+string --> | auto_chopper | --> chopped up string
+           ----------------
+</PRE>
+A chopped up string is a pair of
+<UL>
+<LI>a prefix of the input string, chopped up into words of the language,
+<LI>together with the remaining suffix.
+</UL>
+For example, if the language consists just of the word <KBD>ab</KBD>, the
+input <KBD>ababaab</KBD> is partitioned into a chopped up prefix
+<KBD>[ab,ab]</KBD> and the suffix <KBD>aab</KBD>.
+<P>
+
+The auto_chopper is implemented in theory AutoChopper. The top part of the
+diagram, i.e. the translation of regular expressions into deterministic
+finite automata is still missing.  <P>
+
+<B>WANTED:</B> a theoretically inclined student to formalize a bit of
+undergraduate level automata theory. This could be worth a "Diplom" or an
+M.Sc. It could also be undertaken as a two-person "Fopra".
+</BODY>
+</HTML>