tphols-2011/myhill.pdf
2011-02-19 urbanc included comments by Chunhan
2011-02-17 urbanc first ideas about conclusion
2011-02-16 urbanc minor updated
2011-02-13 zhang More into the second direction
2011-02-10 urbanc more on paper
2011-02-09 urbanc added Xingyuan's changes with the while combinator
2011-02-08 urbanc more direct definitions
2011-02-08 urbanc started to define things more directly
2011-02-08 urbanc small additions
2011-02-07 urbanc added an option fullpaper to IsaMakefile
2011-02-07 urbanc 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 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 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 revised proof of Ardens lemma
2011-01-29 zhang Myhill.thy and Myhill_1.thy changed.
2011-01-28 wu test
2011-01-27 urbanc added my changes again
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 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 zhang ok
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].
less more (0) tip