wu [Thu, 27 Jan 2011 17:37:20 +0000] rev 44
added a recent paper about reg exps and automata
urbanc [Thu, 27 Jan 2011 16:58:11 +0000] rev 43
added my changes again
zhang [Thu, 27 Jan 2011 12:35:06 +0000] rev 42
Trying to solve the confict
zhang [Thu, 27 Jan 2011 11:50:58 +0000] rev 41
a newer version
wu [Thu, 27 Jan 2011 05:39:19 +0000] rev 40
tuned a bit more the last STAR-proof
urbanc [Thu, 27 Jan 2011 00:51:46 +0000] rev 39
tuned a little bit the section about finite partitions
zhang [Wed, 26 Jan 2011 23:39:42 +0000] rev 38
Delete generated
wu [Wed, 26 Jan 2011 22:58:24 +0000] rev 37
ITP-Paper loads Myhill.thy
wu [Wed, 26 Jan 2011 22:51:51 +0000] rev 36
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
urbanc [Wed, 26 Jan 2011 22:23:56 +0000] rev 35
made the theory work under both Isabelle 2009 and 2011
zhang [Wed, 26 Jan 2011 14:13:18 +0000] rev 34
Just checkin
zhang [Wed, 26 Jan 2011 14:12:36 +0000] rev 33
Small modification
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].