zhang [Wed, 26 Jan 2011 13:21:16 +0000] rev 32
ok
zhang [Tue, 25 Jan 2011 12:14:31 +0000] rev 31
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 [Mon, 24 Jan 2011 11:29:55 +0000] rev 30
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].
wu [Fri, 07 Jan 2011 14:25:23 +0000] rev 29
Beautifying of the Other Direction is finished.
wu [Fri, 31 Dec 2010 13:47:53 +0000] rev 28
Rewritten of hard direction once more. To make it looking better.
wu [Tue, 14 Dec 2010 14:31:31 +0000] rev 27
Add new file for the new definition of the hard direction's simplification.
Merging Operation is deleted
All definitions are done. Proof still undone.
urbanc [Fri, 26 Nov 2010 12:34:34 +0000] rev 26
added a recent paper by Tobias Nipkow on regular expressions
urbanc [Fri, 26 Nov 2010 10:53:14 +0000] rev 25
added interesting paper by rutten
urbanc [Thu, 25 Nov 2010 18:54:45 +0000] rev 24
added paper
wu [Thu, 18 Nov 2010 11:39:17 +0000] rev 23
All cases of the Other direction finished