1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
\relax \ifx\hyper@anchor\@undefined\global \let \oldcontentsline\contentsline\gdef \contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}\global \let \oldnewlabel\newlabel\gdef \newlabel#1#2{\newlabelxx{#1}#2}\gdef \newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}\AtEndDocument{\let \contentsline\oldcontentsline\let \newlabel\oldnewlabel}\else\global \let \hyper@last\relax \fi\@writefile{toc}{\contentsline {section}{\numberline {1}Preliminary definitions}{1}{section.1}}\@writefile{toc}{\contentsline {section}{\numberline {2}Direction \emph {\it finite\ partition\ {\emph {$\Rightarrow $}}\ regular\ language}}{5}{section.2}}\newlabel{example_eqns}{{1}{5}{Direction \isa {finite\ partition\ {\isasymRightarrow }\ regular\ language}\relax }{equation.1}{}}\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Proof for this direction}{9}{subsection.2.1}}\@writefile{toc}{\contentsline {section}{\numberline {3}Direction: \emph {\it regular\ language\ {\emph {$\Rightarrow $}}finite\ partition}}{21}{section.3}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}The scheme for this direction}{21}{subsection.3.1}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}A small theory for list difference}{22}{subsection.3.2}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Lemmas for basic cases}{23}{subsection.3.3}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}The case for \emph {\it SEQ}}{24}{subsection.3.4}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.5}The case for \emph {\it ALT}}{26}{subsection.3.5}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.6}The case for \emph {\it STAR}}{27}{subsection.3.6}}\@writefile{toc}{\contentsline {subsection}{\numberline {3.7}The main lemma}{29}{subsection.3.7}}