2011-08-15 polishing of the closure section and conclusion
urbanc [Mon, 15 Aug 2011 21:09:08 +0000] rev 196
polishing of the closure section and conclusion
2011-08-12 small typo
urbanc [Fri, 12 Aug 2011 17:08:58 +0000] rev 195
small typo
2011-08-11 some typos
urbanc [Thu, 11 Aug 2011 23:42:06 +0000] rev 194
some typos
2011-08-11 finished section about derivatives and closure properties
urbanc [Thu, 11 Aug 2011 23:11:39 +0000] rev 193
finished section about derivatives and closure properties
2011-08-11 two interesting papers
urbanc [Thu, 11 Aug 2011 16:55:41 +0000] rev 192
two interesting papers
2011-08-11 slight polishing
urbanc [Thu, 11 Aug 2011 10:26:19 +0000] rev 191
slight polishing
2011-08-09 more on paper
urbanc [Tue, 09 Aug 2011 22:15:11 +0000] rev 190
more on paper
2011-08-09 more on paper and literature
urbanc [Tue, 09 Aug 2011 22:14:41 +0000] rev 189
more on paper and literature
2011-08-05 added paper on partial derivatives
urbanc [Fri, 05 Aug 2011 15:38:28 +0000] rev 188
added paper on partial derivatives
2011-08-05 more on the derivatives section
urbanc [Fri, 05 Aug 2011 05:34:11 +0000] rev 187
more on the derivatives section
2011-08-03 added more to the derivatives section
urbanc [Wed, 03 Aug 2011 17:08:31 +0000] rev 186
added more to the derivatives section
2011-08-03 completed the taging-function section
urbanc [Wed, 03 Aug 2011 13:56:01 +0000] rev 185
completed the taging-function section
2011-08-03 more on the paper
urbanc [Wed, 03 Aug 2011 12:36:23 +0000] rev 184
more on the paper
2011-08-03 cleaned up the proofs in Myhill_2
urbanc [Wed, 03 Aug 2011 00:52:41 +0000] rev 183
cleaned up the proofs in Myhill_2
2011-08-02 a version of the proof which dispenses with the notion of string-subtraction
urbanc [Tue, 02 Aug 2011 15:27:37 +0000] rev 182
a version of the proof which dispenses with the notion of string-subtraction
2011-07-31 some experiments with the proofs in Myhill_2
urbanc [Sun, 31 Jul 2011 10:27:41 +0000] rev 181
some experiments with the proofs in Myhill_2
2011-07-28 added a picture
urbanc [Thu, 28 Jul 2011 17:52:36 +0000] rev 180
added a picture
2011-07-28 small improvements
urbanc [Thu, 28 Jul 2011 14:22:10 +0000] rev 179
small improvements
2011-07-28 added more examles
urbanc [Thu, 28 Jul 2011 11:56:25 +0000] rev 178
added more examles
2011-07-28 more one the paper
urbanc [Thu, 28 Jul 2011 01:12:02 +0000] rev 177
more one the paper
2011-07-27 latest version of the journal paper
urbanc [Wed, 27 Jul 2011 15:29:39 +0000] rev 176
latest version of the journal paper
2011-07-27 polished the introduction
urbanc [Wed, 27 Jul 2011 12:32:28 +0000] rev 175
polished the introduction
2011-07-26 more on the section about derivatives
urbanc [Tue, 26 Jul 2011 18:12:07 +0000] rev 174
more on the section about derivatives
2011-07-26 more on the introduction of the journal paper
urbanc [Tue, 26 Jul 2011 10:58:26 +0000] rev 173
more on the introduction of the journal paper
2011-07-25 more on the journal paper
urbanc [Mon, 25 Jul 2011 18:00:52 +0000] rev 172
more on the journal paper
2011-07-25 added a paper about PEG-parsing and left recursion
urbanc [Mon, 25 Jul 2011 15:40:12 +0000] rev 171
added a paper about PEG-parsing and left recursion
2011-07-25 made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc [Mon, 25 Jul 2011 13:33:38 +0000] rev 170
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
2011-06-03 added boolean grammar
zhang [Fri, 03 Jun 2011 13:59:21 +0000] rev 169
added boolean grammar
2011-06-03 added
zhang [Fri, 03 Jun 2011 13:54:14 +0000] rev 168
added
2011-06-02 added a journal version
urbanc [Thu, 02 Jun 2011 20:02:16 +0000] rev 167
added a journal version
2011-06-02 updated theories and itp-paper
urbanc [Thu, 02 Jun 2011 16:44:35 +0000] rev 166
updated theories and itp-paper
2011-05-31 added missing file
urbanc [Tue, 31 May 2011 20:32:49 +0000] rev 165
added missing file
2011-05-29 added old paper
urbanc [Sun, 29 May 2011 20:01:37 +0000] rev 164
added old paper
2011-05-26 a few more literature places
urbanc [Thu, 26 May 2011 18:39:36 +0000] rev 163
a few more literature places
2011-05-18 added directory for journal version; took uptodate version of the theory files
urbanc [Wed, 18 May 2011 19:54:43 +0000] rev 162
added directory for journal version; took uptodate version of the theory files
2011-05-12 preparation for final paper version
urbanc [Thu, 12 May 2011 05:55:05 +0000] rev 161
preparation for final paper version
2011-05-09 added comments from Chunhan
urbanc [Mon, 09 May 2011 07:25:37 +0000] rev 160
added comments from Chunhan
2011-05-04 edits; sqeezed to 16 pages
urbanc [Wed, 04 May 2011 07:05:59 +0000] rev 159
edits; sqeezed to 16 pages
2011-04-28 paper about formalising parsing; seems to have done what we would like to do....probably also appears at ITP'11
urbanc [Thu, 28 Apr 2011 03:24:20 +0000] rev 158
paper about formalising parsing; seems to have done what we would like to do....probably also appears at ITP'11
2011-04-21 a small change
urbanc [Thu, 21 Apr 2011 22:41:15 +0000] rev 157
a small change
2011-04-21 a few more changes
urbanc [Thu, 21 Apr 2011 12:07:11 +0000] rev 156
a few more changes
2011-04-19 removed experimental code from Matcher
urbanc [Tue, 19 Apr 2011 02:25:21 +0000] rev 155
removed experimental code from Matcher
2011-04-19 implemented most suggestions from the reviewers
urbanc [Tue, 19 Apr 2011 02:19:56 +0000] rev 154
implemented most suggestions from the reviewers
2011-04-06 added literature about parsing
urbanc [Wed, 06 Apr 2011 08:18:23 +0000] rev 153
added literature about parsing
2011-03-25 MN via partial derivatives
urbanc [Fri, 25 Mar 2011 09:42:33 +0000] rev 152
MN via partial derivatives
2011-03-23 moved paper to correct place
urbanc [Wed, 23 Mar 2011 13:33:55 +0000] rev 151
moved paper to correct place
2011-03-23 added paper by Antimirov
urbanc [Wed, 23 Mar 2011 12:22:54 +0000] rev 150
added paper by Antimirov
2011-03-23 added the most current versions of the theories.
urbanc [Wed, 23 Mar 2011 12:17:30 +0000] rev 149
added the most current versions of the theories.
2011-03-15 correct version
urbanc [Tue, 15 Mar 2011 15:53:22 +0000] rev 148
correct version
2011-03-15 deleted wrong version
urbanc [Tue, 15 Mar 2011 15:52:44 +0000] rev 147
deleted wrong version
2011-03-15 added chapter about regular expressions by Sakarovitch (interesting pages are 139 - 142)
urbanc [Tue, 15 Mar 2011 14:29:41 +0000] rev 146
added chapter about regular expressions by Sakarovitch (interesting pages are 139 - 142)
2011-03-15 corrected small typo
urbanc [Tue, 15 Mar 2011 11:04:53 +0000] rev 145
corrected small typo
2011-03-05 slight polishing of the bibliography
urbanc [Sat, 05 Mar 2011 11:42:14 +0000] rev 144
slight polishing of the bibliography
2011-03-05 formalisation of first direction is now only 780 loc
urbanc [Sat, 05 Mar 2011 11:06:39 +0000] rev 143
formalisation of first direction is now only 780 loc
2011-02-26 changed one occurence of tagging function into tagging relation
urbanc [Sat, 26 Feb 2011 15:44:38 +0000] rev 142
changed one occurence of tagging function into tagging relation
2011-02-25 added yacc is dead paper
urbanc [Fri, 25 Feb 2011 12:41:35 +0000] rev 141
added yacc is dead paper
2011-02-24 added a paper about derivatives
urbanc [Thu, 24 Feb 2011 00:37:46 +0000] rev 140
added a paper about derivatives
2011-02-24 added hocroft and ullman book
urbanc [Thu, 24 Feb 2011 00:34:45 +0000] rev 139
added hocroft and ullman book
2011-02-22 three typos
urbanc [Tue, 22 Feb 2011 12:43:05 +0000] rev 138
three typos
2011-02-21 one further polishing
urbanc [Mon, 21 Feb 2011 03:35:39 +0000] rev 137
one further polishing
2011-02-21 final final polishing
urbanc [Mon, 21 Feb 2011 03:33:27 +0000] rev 136
final final polishing
2011-02-21 final polished
urbanc [Mon, 21 Feb 2011 03:30:38 +0000] rev 135
final polished
2011-02-21 chunhan's comments
urbanc [Mon, 21 Feb 2011 02:33:05 +0000] rev 134
chunhan's comments
2011-02-20 minor change
urbanc [Sun, 20 Feb 2011 18:58:34 +0000] rev 133
minor change
2011-02-20 comments by Xingyuan
urbanc [Sun, 20 Feb 2011 18:54:31 +0000] rev 132
comments by Xingyuan
2011-02-20 chunhan's comments
urbanc [Sun, 20 Feb 2011 17:47:54 +0000] rev 131
chunhan's comments
2011-02-20 pre-final version
urbanc [Sun, 20 Feb 2011 13:43:00 +0000] rev 130
pre-final version
2011-02-20 minor
urbanc [Sun, 20 Feb 2011 12:52:35 +0000] rev 129
minor
2011-02-20 finished picture
urbanc [Sun, 20 Feb 2011 12:51:04 +0000] rev 128
finished picture
2011-02-20 seq case finished
urbanc [Sun, 20 Feb 2011 11:14:07 +0000] rev 127
seq case finished
2011-02-20 latest update
urbanc [Sun, 20 Feb 2011 09:54:24 +0000] rev 126
latest update
2011-02-20 added pictures for seq-case
urbanc [Sun, 20 Feb 2011 08:12:13 +0000] rev 125
added pictures for seq-case
2011-02-20 added definition of string prefix and string subtraction
urbanc [Sun, 20 Feb 2011 07:33:54 +0000] rev 124
added definition of string prefix and string subtraction
2011-02-20 polished everywhere...two cases still missing
urbanc [Sun, 20 Feb 2011 06:02:58 +0000] rev 123
polished everywhere...two cases still missing
2011-02-19 my latest version (SEQ and STAR still missing)
urbanc [Sat, 19 Feb 2011 22:05:22 +0000] rev 122
my latest version (SEQ and STAR still missing)
2011-02-19 added directory with the small files and numbers of lines
urbanc [Sat, 19 Feb 2011 21:49:11 +0000] rev 121
added directory with the small files and numbers of lines
2011-02-19 ALT case done
urbanc [Sat, 19 Feb 2011 20:15:59 +0000] rev 120
ALT case done
2011-02-19 first two proofs in 2 direction
urbanc [Sat, 19 Feb 2011 19:27:33 +0000] rev 119
first two proofs in 2 direction
2011-02-19 first proof
urbanc [Sat, 19 Feb 2011 17:10:46 +0000] rev 118
first proof
2011-02-19 updated second direction
urbanc [Sat, 19 Feb 2011 12:01:16 +0000] rev 117
updated second direction
2011-02-19 included comments by Chunhan
urbanc [Sat, 19 Feb 2011 10:23:51 +0000] rev 116
included comments by Chunhan
2011-02-18 added comment from Larry
urbanc [Fri, 18 Feb 2011 15:06:06 +0000] rev 115
added comment from Larry
2011-02-18 updated bib
urbanc [Fri, 18 Feb 2011 14:26:23 +0000] rev 114
updated bib
2011-02-18 polished everything
urbanc [Fri, 18 Feb 2011 12:14:07 +0000] rev 113
polished everything
2011-02-17 more on the conclusion
urbanc [Thu, 17 Feb 2011 21:30:26 +0000] rev 112
more on the conclusion
2011-02-17 first ideas about conclusion
urbanc [Thu, 17 Feb 2011 13:25:29 +0000] rev 111
first ideas about conclusion
2011-02-17 completed first direction
urbanc [Thu, 17 Feb 2011 11:42:16 +0000] rev 110
completed first direction
2011-02-16 minor updated
urbanc [Wed, 16 Feb 2011 12:25:53 +0000] rev 109
minor updated
2011-02-16 filled details in one place
urbanc [Wed, 16 Feb 2011 06:51:58 +0000] rev 108
filled details in one place
2011-02-15 updated paper
urbanc [Tue, 15 Feb 2011 14:17:31 +0000] rev 107
updated paper
2011-02-15 updated paper
urbanc [Tue, 15 Feb 2011 12:01:29 +0000] rev 106
updated paper
2011-02-15 updated paper
urbanc [Tue, 15 Feb 2011 10:37:56 +0000] rev 105
updated paper
2011-02-15 updated paper
urbanc [Tue, 15 Feb 2011 08:08:04 +0000] rev 104
updated paper
2011-02-14 updated
urbanc [Mon, 14 Feb 2011 23:10:44 +0000] rev 103
updated
2011-02-14 added definition of DERIV and delta
urbanc [Mon, 14 Feb 2011 11:12:01 +0000] rev 102
added definition of DERIV and delta
2011-02-14 updated paper
urbanc [Mon, 14 Feb 2011 09:38:18 +0000] rev 101
updated paper
2011-02-14 updated
urbanc [Mon, 14 Feb 2011 07:42:16 +0000] rev 100
updated
2011-02-13 More into the second direction
zhang [Sun, 13 Feb 2011 10:36:53 +0000] rev 99
More into the second direction
2011-02-11 included comments by Xingyuan
urbanc [Fri, 11 Feb 2011 13:30:37 +0000] rev 98
included comments by Xingyuan
2011-02-11 slightly streamlined the proof
urbanc [Fri, 11 Feb 2011 12:13:35 +0000] rev 97
slightly streamlined the proof
2011-02-10 simplified a bit the proof
urbanc [Thu, 10 Feb 2011 21:00:40 +0000] rev 96
simplified a bit the proof
2011-02-10 more things
urbanc [Thu, 10 Feb 2011 13:10:16 +0000] rev 95
more things
2011-02-10 latest on the paper
urbanc [Thu, 10 Feb 2011 12:32:45 +0000] rev 94
latest on the paper
2011-02-10 more on the paper
urbanc [Thu, 10 Feb 2011 08:40:38 +0000] rev 93
more on the paper
2011-02-10 more on paper
urbanc [Thu, 10 Feb 2011 05:57:56 +0000] rev 92
more on paper
2011-02-09 added Xingyuan's changes with the while combinator
urbanc [Wed, 09 Feb 2011 12:34:30 +0000] rev 91
added Xingyuan's changes with the while combinator
2011-02-09 added an example
urbanc [Wed, 09 Feb 2011 09:46:59 +0000] rev 90
added an example
2011-02-09 a bit more on the paper
urbanc [Wed, 09 Feb 2011 07:27:30 +0000] rev 89
a bit more on the paper
2011-02-09 added something about Setalt and folds
urbanc [Wed, 09 Feb 2011 06:09:46 +0000] rev 88
added something about Setalt and folds
2011-02-09 deleted the non_empty invariant
urbanc [Wed, 09 Feb 2011 04:54:23 +0000] rev 87
deleted the non_empty invariant
2011-02-09 tuned comments and names in Myhill_1
urbanc [Wed, 09 Feb 2011 04:50:18 +0000] rev 86
tuned comments and names in Myhill_1
2011-02-09 separated the definition of folds into a separate file
urbanc [Wed, 09 Feb 2011 03:52:28 +0000] rev 85
separated the definition of folds into a separate file
2011-02-09 saved a copy of the current Myhill for reference
urbanc [Wed, 09 Feb 2011 03:33:30 +0000] rev 84
saved a copy of the current Myhill for reference
2011-02-08 a bit more on the paper
urbanc [Tue, 08 Feb 2011 19:54:23 +0000] rev 83
a bit more on the paper
2011-02-08 added coments about functions
urbanc [Tue, 08 Feb 2011 18:04:54 +0000] rev 82
added coments about functions
2011-02-08 more direct definitions
urbanc [Tue, 08 Feb 2011 16:49:18 +0000] rev 81
more direct definitions
2011-02-08 deleted lam_of
urbanc [Tue, 08 Feb 2011 15:59:47 +0000] rev 80
deleted lam_of
2011-02-08 started to define things more directly
urbanc [Tue, 08 Feb 2011 15:50:26 +0000] rev 79
started to define things more directly
2011-02-08 More explaination on equational system
zhang [Tue, 08 Feb 2011 12:01:28 +0000] rev 78
More explaination on equational system
2011-02-08 small additions
urbanc [Tue, 08 Feb 2011 09:51:49 +0000] rev 77
small additions
2011-02-08 added an abbreviation for folds ALT NULL
urbanc [Tue, 08 Feb 2011 09:51:27 +0000] rev 76
added an abbreviation for folds ALT NULL
2011-02-07 parts of the 3 section
urbanc [Mon, 07 Feb 2011 20:30:10 +0000] rev 75
parts of the 3 section
2011-02-07 added bib-file
urbanc [Mon, 07 Feb 2011 13:17:01 +0000] rev 74
added bib-file
2011-02-07 More into first direction
zhang [Mon, 07 Feb 2011 13:08:09 +0000] rev 73
More into first direction
2011-02-07 added an option fullpaper to IsaMakefile
urbanc [Mon, 07 Feb 2011 11:12:36 +0000] rev 72
added an option fullpaper to IsaMakefile
2011-02-07 more on the paper
urbanc [Mon, 07 Feb 2011 10:23:23 +0000] rev 71
more on the paper
2011-02-06 slightly more on the paper
urbanc [Sun, 06 Feb 2011 11:21:12 +0000] rev 70
slightly more on the paper
2011-02-06 A formal presentation of automaton and Myhill-Nerrode theorem added to serve as a basis for further discussion
zhang [Sun, 06 Feb 2011 10:28:29 +0000] rev 69
A formal presentation of automaton and Myhill-Nerrode theorem added to serve as a basis for further discussion
2011-02-05 Check in Myhill.thy before trying another way to explain DFA
zhang [Sat, 05 Feb 2011 13:56:50 +0000] rev 68
Check in Myhill.thy before trying another way to explain DFA
2011-02-05 more intro
urbanc [Sat, 05 Feb 2011 09:54:52 +0000] rev 67
more intro
2011-02-04 more on the introduction
urbanc [Fri, 04 Feb 2011 22:54:29 +0000] rev 66
more on the introduction
2011-02-04 exercise about arden from TU Munich
urbanc [Fri, 04 Feb 2011 13:33:18 +0000] rev 65
exercise about arden from TU Munich
2011-02-04 Added something to Myhill.thy, trying to explain the relationship between finite automata and language partition.
zhang [Fri, 04 Feb 2011 13:02:00 +0000] rev 64
Added something to Myhill.thy, trying to explain the relationship between finite automata and language partition.
2011-02-03 Myhill_2.thy added
zhang [Thu, 03 Feb 2011 12:44:46 +0000] rev 63
Myhill_2.thy added
2011-02-03 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.
zhang [Thu, 03 Feb 2011 12:00:06 +0000] rev 62
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 more to the intro
urbanc [Thu, 03 Feb 2011 09:54:19 +0000] rev 61
more to the intro
2011-02-03 a bit more tuning on the introduction
urbanc [Thu, 03 Feb 2011 05:38:47 +0000] rev 60
a bit more tuning on the introduction
2011-02-02 more on the intro
urbanc [Wed, 02 Feb 2011 15:43:22 +0000] rev 59
more on the intro
2011-02-02 a little bit in the introduction
urbanc [Wed, 02 Feb 2011 13:54:07 +0000] rev 58
a little bit in the introduction
2011-02-02 Myhill.pdf modified
zhang [Wed, 02 Feb 2011 13:25:09 +0000] rev 57
Myhill.pdf modified
2011-02-02 removed the inductive definition of Star and replaced it by a definition in terms of pow
urbanc [Wed, 02 Feb 2011 06:05:12 +0000] rev 56
removed the inductive definition of Star and replaced it by a definition in terms of pow
2011-01-31 Myhill.thy IsabelleMakefile modified
zhang [Mon, 31 Jan 2011 14:51:47 +0000] rev 55
Myhill.thy IsabelleMakefile modified
2011-01-31 a bit more on the paper
urbanc [Mon, 31 Jan 2011 12:54:31 +0000] rev 54
a bit more on the paper
2011-01-30 small typo
urbanc [Sun, 30 Jan 2011 17:24:37 +0000] rev 53
small typo
2011-01-30 tuning of the syntax; needs the stmaryrd latex package
urbanc [Sun, 30 Jan 2011 17:21:53 +0000] rev 52
tuning of the syntax; needs the stmaryrd latex package
2011-01-30 some tuning of the paper
urbanc [Sun, 30 Jan 2011 17:09:02 +0000] rev 51
some tuning of the paper
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
2010-11-10 added my slides
urbanc [Wed, 10 Nov 2010 11:49:45 +0000] rev 20
added my slides
2010-11-08 slight tuning of proof by Chunhan
urbanc [Mon, 08 Nov 2010 01:13:09 +0000] rev 19
slight tuning of proof by Chunhan
2010-11-06 the ALT case is done;
wu [Sat, 06 Nov 2010 23:31:53 +0000] rev 18
the ALT case is done; the other two cases: the relation is defined by not proved on inj part.
2010-11-03 added more experiments
urbanc [Wed, 03 Nov 2010 22:08:50 +0000] rev 17
added more experiments
2010-11-03 added initial slides for informal talk in Cambridge
urbanc [Wed, 03 Nov 2010 21:42:44 +0000] rev 16
added initial slides for informal talk in Cambridge
2010-10-26 added slides of chunhan
urbanc [Tue, 26 Oct 2010 23:09:31 +0000] rev 15
added slides of chunhan
2010-10-26 more experiments
urbanc [Tue, 26 Oct 2010 13:01:22 +0000] rev 14
more experiments
2010-10-24 a few more experiments, but no proof for the ALT-case
urbanc [Sun, 24 Oct 2010 01:17:44 +0000] rev 13
a few more experiments, but no proof for the ALT-case
2010-10-23 add some proofs about the other direction
wu [Sat, 23 Oct 2010 12:51:38 +0000] rev 12
add some proofs about the other direction 1: the NULL case 2: the EMPTY case 3: the atomic CHAR c case
2010-10-22 deleted two unnecessary lemmas
urbanc [Fri, 22 Oct 2010 19:43:56 +0000] rev 11
deleted two unnecessary lemmas
2010-10-22 added a paper by Constable about the Myhill-Nerode in Nuprl using DFA and a paper by tobias about RegExp->DFA translation
urbanc [Fri, 22 Oct 2010 10:45:01 +0000] rev 10
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 deleted the test
urbanc [Thu, 21 Oct 2010 15:35:03 +0000] rev 9
deleted the test
2010-10-21 tried at the end to prove the other direction (failed at the moment)
urbanc [Thu, 21 Oct 2010 15:06:30 +0000] rev 8
tried at the end to prove the other direction (failed at the moment)
2010-10-21 deleted the matcher ate the beginning; made it to work with stable Isabelle and the development version
urbanc [Thu, 21 Oct 2010 13:42:08 +0000] rev 7
deleted the matcher ate the beginning; made it to work with stable Isabelle and the development version
2010-10-20 former version has a ugly usage of "overloaded";
wu [Wed, 20 Oct 2010 14:11:14 +0000] rev 6
former version has a ugly usage of "overloaded"; changing this using "overloading" by chunhan
2010-10-19 added a file about the easy closure properties of regular sets (the difficult parts, like complement, are missing)
urbanc [Tue, 19 Oct 2010 11:51:05 +0000] rev 5
added a file about the easy closure properties of regular sets (the difficult parts, like complement, are missing)
(0) -192 +192 tip