2011-01-30 revised proof of Ardens lemma
urbanc [Sun, 30 Jan 2011 16:59:57 +0000] rev 50
revised proof of Ardens lemma
2011-01-30 Illustration added together with renewed explainations for case STAR.
zhang [Sun, 30 Jan 2011 12:22:07 +0000] rev 49
Illustration added together with renewed explainations for case STAR.
2011-01-29 Myhill.thy and Myhill_1.thy changed.
zhang [Sat, 29 Jan 2011 11:41:17 +0000] rev 48
Myhill.thy and Myhill_1.thy changed.
2011-01-28 slightly tuned the main lemma and the finiteness proofs
urbanc [Fri, 28 Jan 2011 19:17:40 +0000] rev 47
slightly tuned the main lemma and the finiteness proofs
2011-01-28 test
wu [Fri, 28 Jan 2011 12:53:01 +0000] rev 46
test
2011-01-28 More improvement
zhang [Fri, 28 Jan 2011 11:52:11 +0000] rev 45
More improvement
2011-01-27 added a recent paper about reg exps and automata
wu [Thu, 27 Jan 2011 17:37:20 +0000] rev 44
added a recent paper about reg exps and automata
2011-01-27 added my changes again
urbanc [Thu, 27 Jan 2011 16:58:11 +0000] rev 43
added my changes again
2011-01-27 Trying to solve the confict
zhang [Thu, 27 Jan 2011 12:35:06 +0000] rev 42
Trying to solve the confict
2011-01-27 a newer version
zhang [Thu, 27 Jan 2011 11:50:58 +0000] rev 41
a newer version
2011-01-27 tuned a bit more the last STAR-proof
wu [Thu, 27 Jan 2011 05:39:19 +0000] rev 40
tuned a bit more the last STAR-proof
2011-01-27 tuned a little bit the section about finite partitions
urbanc [Thu, 27 Jan 2011 00:51:46 +0000] rev 39
tuned a little bit the section about finite partitions
2011-01-26 Delete generated
zhang [Wed, 26 Jan 2011 23:39:42 +0000] rev 38
Delete generated
2011-01-26 ITP-Paper loads Myhill.thy
wu [Wed, 26 Jan 2011 22:58:24 +0000] rev 37
ITP-Paper loads Myhill.thy
2011-01-26 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
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
2011-01-26 made the theory work under both Isabelle 2009 and 2011
urbanc [Wed, 26 Jan 2011 22:23:56 +0000] rev 35
made the theory work under both Isabelle 2009 and 2011
2011-01-26 Just checkin
zhang [Wed, 26 Jan 2011 14:13:18 +0000] rev 34
Just checkin
2011-01-26 Small modification
zhang [Wed, 26 Jan 2011 14:12:36 +0000] rev 33
Small modification
2011-01-26 ok
zhang [Wed, 26 Jan 2011 13:21:16 +0000] rev 32
ok
2011-01-25 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 [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
2011-01-24 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 [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].
2011-01-07 Beautifying of the Other Direction is finished.
wu [Fri, 07 Jan 2011 14:25:23 +0000] rev 29
Beautifying of the Other Direction is finished.
2010-12-31 Rewritten of hard direction once more. To make it looking better.
wu [Fri, 31 Dec 2010 13:47:53 +0000] rev 28
Rewritten of hard direction once more. To make it looking better.
2010-12-14 Add new file for the new definition of the hard direction's simplification.
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.
2010-11-26 added a recent paper by Tobias Nipkow on regular expressions
urbanc [Fri, 26 Nov 2010 12:34:34 +0000] rev 26
added a recent paper by Tobias Nipkow on regular expressions
2010-11-26 added interesting paper by rutten
urbanc [Fri, 26 Nov 2010 10:53:14 +0000] rev 25
added interesting paper by rutten
2010-11-25 added paper
urbanc [Thu, 25 Nov 2010 18:54:45 +0000] rev 24
added paper
2010-11-18 All cases of the Other direction finished
wu [Thu, 18 Nov 2010 11:39:17 +0000] rev 23
All cases of the Other direction finished
2010-11-10 added a test file
urbanc [Wed, 10 Nov 2010 11:59:29 +0000] rev 22
added a test file
2010-11-10 my slides from the talk in Cambridge
urbanc [Wed, 10 Nov 2010 11:53:07 +0000] rev 21
my slides from the talk in Cambridge
(0) -30 +30 +50 +100 +300 tip