Mercurial Mercurial > hg > regexp / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tphols-2011/generated/root.toc
author zhang
Mon, 24 Jan 2011 11:29:55 +0000
changeset 30 f5db9e08effc
permissions -rw-r--r--
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     1
 
\contentsline {section}{\numberline {1}Preliminary definitions}{1}{section.1}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     2
 
\contentsline {section}{\numberline {2}Direction \emph {\it finite\ partition\ {\emph {$\Rightarrow $}}\ regular\ language}}{5}{section.2}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     3
 
\contentsline {subsection}{\numberline {2.1}Proof for this direction}{9}{subsection.2.1}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     4
 
\contentsline {section}{\numberline {3}Direction: \emph {\it regular\ language\ {\emph {$\Rightarrow $}}finite\ partition}}{21}{section.3}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     5
 
\contentsline {subsection}{\numberline {3.1}The scheme for this direction}{21}{subsection.3.1}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     6
 
\contentsline {subsection}{\numberline {3.2}A small theory for list difference}{22}{subsection.3.2}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     7
 
\contentsline {subsection}{\numberline {3.3}Lemmas for basic cases}{23}{subsection.3.3}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     8
 
\contentsline {subsection}{\numberline {3.4}The case for \emph {\it SEQ}}{24}{subsection.3.4}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
     9
 
\contentsline {subsection}{\numberline {3.5}The case for \emph {\it ALT}}{26}{subsection.3.5}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
    10
 
\contentsline {subsection}{\numberline {3.6}The case for \emph {\it STAR}}{27}{subsection.3.6}
f5db9e08effc Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
parents:
diff changeset 
    11
 
\contentsline {subsection}{\numberline {3.7}The main lemma}{29}{subsection.3.7}
regexp