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.
Myhill.thy
author zhang
Thu, 03 Feb 2011 12:00:06 +0000
changeset 62 d94209ad2880
parent 57 76ab7c09d575
child 64 b69d4e04e64a
permissions -rw-r--r--
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31
b6815473ee2e 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
zhang
parents: 30
diff changeset 
     1
 
theory Myhill
62
d94209ad2880 Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
zhang
parents: 57
diff changeset 
     2
 
  imports Myhill_2
31
b6815473ee2e 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
zhang
parents: 30
diff changeset 
     3
 
begin
b6815473ee2e 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
zhang
parents: 30
diff changeset 
     4
 







48






61d9684a557a
Myhill.thy and Myhill_1.thy changed.



zhang


parents: 
47

diff
changeset




     5


section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}








31






b6815473ee2e
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



zhang


parents: 
30

diff
changeset




     6














b6815473ee2e
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



zhang


parents: 
30

diff
changeset




     7


text {*








62






d94209ad2880
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.



zhang


parents: 
57

diff
changeset




     8


  It is now the time for use to discuss further about the way.








55






d71424eb5d0c
Myhill.thy IsabelleMakefile modified



zhang


parents: 
49

diff
changeset




     9


  *}













d71424eb5d0c
Myhill.thy IsabelleMakefile modified



zhang


parents: 
49

diff
changeset




    10









31






b6815473ee2e
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



zhang


parents: 
30

diff
changeset




    11


end















regexp