2011-02-19 urbanc first two proofs in 2 direction
2011-02-19 urbanc first proof
2011-02-19 urbanc updated second direction
2011-02-19 urbanc included comments by Chunhan
2011-02-18 urbanc added comment from Larry
2011-02-18 urbanc updated bib
2011-02-18 urbanc polished everything
2011-02-17 urbanc more on the conclusion
2011-02-17 urbanc first ideas about conclusion
2011-02-17 urbanc completed first direction
2011-02-16 urbanc minor updated
2011-02-16 urbanc filled details in one place
2011-02-15 urbanc updated paper
2011-02-15 urbanc updated paper
2011-02-15 urbanc updated paper
2011-02-15 urbanc updated paper
2011-02-14 urbanc updated
2011-02-14 urbanc added definition of DERIV and delta
2011-02-14 urbanc updated paper
2011-02-14 urbanc updated
2011-02-13 zhang More into the second direction
2011-02-11 urbanc included comments by Xingyuan
2011-02-11 urbanc slightly streamlined the proof
2011-02-10 urbanc simplified a bit the proof
2011-02-10 urbanc more things
2011-02-10 urbanc latest on the paper
2011-02-10 urbanc more on the paper
2011-02-10 urbanc more on paper
2011-02-09 urbanc added Xingyuan's changes with the while combinator
2011-02-09 urbanc added an example
2011-02-09 urbanc a bit more on the paper
2011-02-09 urbanc added something about Setalt and folds
2011-02-09 urbanc deleted the non_empty invariant
2011-02-09 urbanc tuned comments and names in Myhill_1
2011-02-09 urbanc separated the definition of folds into a separate file
2011-02-09 urbanc saved a copy of the current Myhill for reference
2011-02-08 urbanc a bit more on the paper
2011-02-08 urbanc added coments about functions
2011-02-08 urbanc more direct definitions
2011-02-08 urbanc deleted lam_of
2011-02-08 urbanc started to define things more directly
2011-02-08 zhang More explaination on equational system
2011-02-08 urbanc small additions
2011-02-08 urbanc added an abbreviation for folds ALT NULL
2011-02-07 urbanc parts of the 3 section
2011-02-07 urbanc added bib-file
2011-02-07 zhang More into first direction
2011-02-07 urbanc added an option fullpaper to IsaMakefile
2011-02-07 urbanc more on the paper
2011-02-06 urbanc slightly more on the paper
2011-02-06 zhang A formal presentation of automaton and Myhill-Nerrode theorem added to serve as a basis for further discussion
2011-02-05 zhang Check in Myhill.thy before trying another way to explain DFA
2011-02-05 urbanc more intro
2011-02-04 urbanc more on the introduction
2011-02-04 urbanc exercise about arden from TU Munich
2011-02-04 zhang Added something to Myhill.thy, trying to explain the relationship between finite automata and language partition.
2011-02-03 zhang Myhill_2.thy added
2011-02-03 zhang 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.
2011-02-03 urbanc more to the intro
2011-02-03 urbanc a bit more tuning on the introduction
2011-02-02 urbanc more on the intro
2011-02-02 urbanc a little bit in the introduction
2011-02-02 zhang Myhill.pdf modified
2011-02-02 urbanc removed the inductive definition of Star and replaced it by a definition in terms of pow
2011-01-31 zhang Myhill.thy IsabelleMakefile modified
2011-01-31 urbanc a bit more on the paper
2011-01-30 urbanc small typo
2011-01-30 urbanc tuning of the syntax; needs the stmaryrd latex package
2011-01-30 urbanc some tuning of the paper
2011-01-30 urbanc revised proof of Ardens lemma
2011-01-30 zhang Illustration added together with renewed explainations for case STAR.
2011-01-29 zhang Myhill.thy and Myhill_1.thy changed.
2011-01-28 urbanc slightly tuned the main lemma and the finiteness proofs
2011-01-28 wu test
2011-01-28 zhang More improvement
2011-01-27 wu added a recent paper about reg exps and automata
2011-01-27 urbanc added my changes again
2011-01-27 zhang Trying to solve the confict
2011-01-27 zhang a newer version
2011-01-27 wu tuned a bit more the last STAR-proof
2011-01-27 urbanc tuned a little bit the section about finite partitions
2011-01-26 zhang Delete generated
2011-01-26 wu ITP-Paper loads Myhill.thy
2011-01-26 wu added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
2011-01-26 urbanc made the theory work under both Isabelle 2009 and 2011
2011-01-26 zhang Just checkin
2011-01-26 zhang Small modification
2011-01-26 zhang ok
2011-01-25 zhang 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 zhang 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 wu Beautifying of the Other Direction is finished.
2010-12-31 wu Rewritten of hard direction once more. To make it looking better.
2010-12-14 wu Add new file for the new definition of the hard direction's simplification.
2010-11-26 urbanc added a recent paper by Tobias Nipkow on regular expressions
2010-11-26 urbanc added interesting paper by rutten
2010-11-25 urbanc added paper
2010-11-18 wu All cases of the Other direction finished
2010-11-10 urbanc added a test file
2010-11-10 urbanc my slides from the talk in Cambridge
2010-11-10 urbanc added my slides
2010-11-08 urbanc slight tuning of proof by Chunhan
2010-11-06 wu the ALT case is done;
2010-11-03 urbanc added more experiments
2010-11-03 urbanc added initial slides for informal talk in Cambridge
2010-10-26 urbanc added slides of chunhan
2010-10-26 urbanc more experiments
2010-10-24 urbanc a few more experiments, but no proof for the ALT-case
2010-10-23 wu add some proofs about the other direction
2010-10-22 urbanc deleted two unnecessary lemmas
2010-10-22 urbanc added a paper by Constable about the Myhill-Nerode in Nuprl using DFA and a paper by tobias about RegExp->DFA translation
2010-10-21 urbanc deleted the test
2010-10-21 urbanc tried at the end to prove the other direction (failed at the moment)
2010-10-21 urbanc deleted the matcher ate the beginning; made it to work with stable Isabelle and the development version
2010-10-20 wu former version has a ugly usage of "overloaded";
2010-10-19 urbanc added a file about the easy closure properties of regular sets (the difficult parts, like complement, are missing)
2010-10-07 wu Add a test file, after testing, this file can be deleted.
2010-10-03 urbanc added simple regexp matcher from Slind et al
2010-10-03 urbanc test
2010-10-03 urbanc added literature
2010-10-03 urbanc added initial version by Chunhan
(0) +120 tip