Christian Urban <christian dot urban at kcl dot ac dot uk> [Sun, 22 Dec 2013 07:37:26 +0000] rev 393
added
Christian Urban <christian dot urban at kcl dot ac dot uk> [Sun, 10 Nov 2013 17:07:19 +0000] rev 392
added small comments
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 03 Oct 2013 15:29:03 +0100] rev 391
added slides
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 02 Oct 2013 13:17:32 +0100] rev 390
added new slides
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 27 Sep 2013 09:20:58 +0100] rev 389
added paper by Tobias
Christian Urban <christian dot urban at kcl dot ac dot uk> [Tue, 17 Sep 2013 11:21:58 +0100] rev 388
new version
Christian Urban <christian dot urban at kcl dot ac dot uk> [Sat, 14 Sep 2013 14:08:19 +0100] rev 387
more changes for final submission
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 12 Sep 2013 17:20:48 +0100] rev 386
soem small changes
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 12 Sep 2013 10:34:11 +0200] rev 385
updated to new Isabelle
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 11 Jul 2013 16:46:05 +0100] rev 384
comment by Chunhan
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 11 Jul 2013 12:07:11 +0100] rev 383
some more polishing
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 10 Jul 2013 17:59:00 +0100] rev 382
polished
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 10 Jul 2013 17:47:30 +0100] rev 381
added modified version adn answer to the reviewers
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 10 Jul 2013 13:28:24 +0100] rev 380
added coquand siles paper
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 05 Jul 2013 17:19:17 +0100] rev 379
polished more and updated to new isabelle
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 05 Jul 2013 12:07:48 +0100] rev 378
deleted utm-work from the repository
Christian Urban <christian dot urban at kcl dot ac dot uk> [Mon, 04 Mar 2013 21:01:55 +0000] rev 377
updated
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 01 Mar 2013 17:28:25 +0000] rev 376
updated
Christian Urban <christian dot urban at kcl dot ac dot uk> [Fri, 01 Mar 2013 17:13:32 +0000] rev 375
adapted to JAR
Christian Urban <christian dot urban at kcl dot ac dot uk> [Wed, 12 Dec 2012 11:45:04 +0000] rev 374
slight changes
Christian Urban <christian dot urban at kcl dot ac dot uk> [Thu, 06 Dec 2012 16:32:03 +0000] rev 373
added pip to a new repository
Christian Urban <christian dot urban at kcl dot ac dot uk> [Mon, 03 Dec 2012 08:16:58 +0000] rev 372
made changes and updates to the journal paper
zhang [Mon, 15 Oct 2012 13:23:52 +0000] rev 371
Some illustration added together with more explanations.
zhang [Sat, 29 Sep 2012 12:38:12 +0000] rev 370
Initial upload of the formal construction of Universal Turing Machine.
urbanc [Thu, 30 Aug 2012 08:30:57 +0000] rev 369
small change
urbanc [Wed, 29 Aug 2012 13:09:36 +0000] rev 368
some addition to the MN-paper
urbanc [Wed, 29 Aug 2012 13:05:46 +0000] rev 367
for slides
urbanc [Wed, 29 Aug 2012 13:05:25 +0000] rev 366
added slides for talk at Imperial
wu [Mon, 13 Aug 2012 12:11:50 +0000] rev 365
(none)
wu [Mon, 13 Aug 2012 12:08:52 +0000] rev 364
add comments by christian
wu [Mon, 13 Aug 2012 10:37:37 +0000] rev 363
Slightly modifications.
zhang [Fri, 10 Aug 2012 13:57:41 +0000] rev 362
Slides modified
zhang [Fri, 10 Aug 2012 13:54:21 +0000] rev 361
IsaMakefile modified
urbanc [Thu, 28 Jun 2012 11:25:26 +0000] rev 360
added some slides for an informal talk about PIP
urbanc [Thu, 21 Jun 2012 15:04:48 +0000] rev 359
corrected reference to Rostedt article
urbanc [Thu, 24 May 2012 11:37:03 +0000] rev 358
small typo in the itp-12 paper
urbanc [Fri, 11 May 2012 13:26:50 +0000] rev 357
typo
urbanc [Wed, 09 May 2012 13:42:23 +0000] rev 356
updated
urbanc [Wed, 09 May 2012 13:41:35 +0000] rev 355
comments by Xingyuan
urbanc [Thu, 03 May 2012 08:52:03 +0000] rev 354
some small editing
urbanc [Thu, 03 May 2012 00:43:57 +0000] rev 353
tuned paragraph on multiprocesors
urbanc [Wed, 02 May 2012 13:13:47 +0000] rev 352
added section about PINTOS and rewritten multi-processor section
urbanc [Mon, 30 Apr 2012 15:32:34 +0000] rev 351
slightly changed the definition of holdends and detached
urbanc [Mon, 23 Apr 2012 08:01:37 +0000] rev 350
made changes for another journal submission of the MN-paper
urbanc [Fri, 20 Apr 2012 14:15:36 +0000] rev 349
changes to get the files through for CU
urbanc [Fri, 20 Apr 2012 11:45:06 +0000] rev 348
made changes for another journal submission of the MH-paper
zhang [Fri, 20 Apr 2012 11:27:49 +0000] rev 347
Intuitive definition of "detached" is added to PrioG.thy.
urbanc [Tue, 17 Apr 2012 15:55:37 +0000] rev 346
added an acknowledgement
urbanc [Tue, 17 Apr 2012 15:45:05 +0000] rev 345
some small tuning
urbanc [Tue, 17 Apr 2012 15:37:03 +0000] rev 344
some small improvements
urbanc [Mon, 16 Apr 2012 15:16:02 +0000] rev 343
???-marks
urbanc [Mon, 16 Apr 2012 15:08:24 +0000] rev 342
changes requested by the reviewers
urbanc [Mon, 16 Apr 2012 12:54:08 +0000] rev 341
polished
zhang [Mon, 16 Apr 2012 08:48:20 +0000] rev 340
The result for "Set" operation gets strengthened.
urbanc [Sun, 15 Apr 2012 21:53:12 +0000] rev 339
added some of the comments of the reviewers and made it compile with current Isabelle
urbanc [Fri, 13 Apr 2012 13:12:43 +0000] rev 338
made the changes thes 2nd referee suggested and made it to compile again
urbanc [Tue, 06 Mar 2012 11:30:45 +0000] rev 337
typo
urbanc [Tue, 28 Feb 2012 13:13:32 +0000] rev 336
fixed typo
urbanc [Mon, 27 Feb 2012 18:53:53 +0000] rev 335
typo
urbanc [Wed, 22 Feb 2012 13:25:49 +0000] rev 334
partially updated conference paper; slightly tuned journal paper
urbanc [Mon, 20 Feb 2012 11:02:50 +0000] rev 333
some polishing of the repository
urbanc [Thu, 16 Feb 2012 08:12:01 +0000] rev 332
one typo
urbanc [Tue, 14 Feb 2012 04:33:31 +0000] rev 331
changes by Xingyuan
urbanc [Tue, 14 Feb 2012 04:14:18 +0000] rev 330
changed
urbanc [Tue, 14 Feb 2012 04:13:15 +0000] rev 329
live
urbanc [Tue, 14 Feb 2012 03:26:18 +0000] rev 328
live
urbanc [Tue, 14 Feb 2012 02:55:47 +0000] rev 327
draft
urbanc [Tue, 14 Feb 2012 02:53:34 +0000] rev 326
draft
urbanc [Tue, 14 Feb 2012 02:24:09 +0000] rev 325
key lemma
urbanc [Tue, 14 Feb 2012 00:27:47 +0000] rev 324
fixed 1st paragraph
urbanc [Tue, 14 Feb 2012 00:11:17 +0000] rev 323
1st paragraph
urbanc [Mon, 13 Feb 2012 23:50:37 +0000] rev 322
1st paragraph
urbanc [Mon, 13 Feb 2012 23:31:40 +0000] rev 321
polished implementation
zhang [Mon, 13 Feb 2012 22:45:06 +0000] rev 320
Line numbers added.
urbanc [Mon, 13 Feb 2012 22:17:54 +0000] rev 319
conclusion done
urbanc [Mon, 13 Feb 2012 22:17:26 +0000] rev 318
more conclusion
urbanc [Mon, 13 Feb 2012 22:03:36 +0000] rev 317
more conclusion
urbanc [Mon, 13 Feb 2012 21:34:19 +0000] rev 316
more conclusion
urbanc [Mon, 13 Feb 2012 20:57:02 +0000] rev 315
more conclusion
urbanc [Mon, 13 Feb 2012 19:33:03 +0000] rev 314
some parts of the conclusion
urbanc [Mon, 13 Feb 2012 15:42:45 +0000] rev 313
proof idea
urbanc [Mon, 13 Feb 2012 15:35:08 +0000] rev 312
added implementation section
urbanc [Mon, 13 Feb 2012 10:57:47 +0000] rev 311
merged Xingyuan's changes
urbanc [Mon, 13 Feb 2012 10:44:42 +0000] rev 310
polished
urbanc [Mon, 13 Feb 2012 05:41:53 +0000] rev 309
more on the paper
urbanc [Mon, 13 Feb 2012 04:22:52 +0000] rev 308
more on the paper
urbanc [Mon, 13 Feb 2012 03:31:40 +0000] rev 307
assumptions
urbanc [Mon, 13 Feb 2012 00:06:59 +0000] rev 306
some polishing
urbanc [Sun, 12 Feb 2012 23:25:49 +0000] rev 305
some polishing
urbanc [Sun, 12 Feb 2012 23:20:06 +0000] rev 304
contribution section
zhang [Sun, 12 Feb 2012 15:12:50 +0000] rev 303
Correct a mistake.
zhang [Sun, 12 Feb 2012 15:05:57 +0000] rev 302
runing_inversion_3 added.
urbanc [Sun, 12 Feb 2012 14:58:47 +0000] rev 301
lates
urbanc [Sun, 12 Feb 2012 11:30:17 +0000] rev 300
correct RAG
urbanc [Sun, 12 Feb 2012 05:06:59 +0000] rev 299
small polishing
urbanc [Sun, 12 Feb 2012 04:45:20 +0000] rev 298
completed model section; vt has only state as argument
urbanc [Sat, 11 Feb 2012 19:39:50 +0000] rev 297
added picture
urbanc [Sat, 11 Feb 2012 12:29:52 +0000] rev 296
spell check; release
urbanc [Sat, 11 Feb 2012 10:09:39 +0000] rev 295
fixed problem with back
urbanc [Sat, 11 Feb 2012 09:34:46 +0000] rev 294
renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc [Sat, 11 Feb 2012 09:14:14 +0000] rev 293
some polishing
urbanc [Sat, 11 Feb 2012 08:16:11 +0000] rev 292
fixed problem with Latexsugar
urbanc [Fri, 10 Feb 2012 21:01:03 +0000] rev 291
more on paper; modified schs functions; it is still compatible with the old definition
urbanc [Fri, 10 Feb 2012 11:30:47 +0000] rev 290
more on paper
urbanc [Thu, 09 Feb 2012 16:34:18 +0000] rev 289
attempt to fix problem by Xingyuan
urbanc [Thu, 09 Feb 2012 15:00:19 +0000] rev 288
changes by Xingyuan
urbanc [Thu, 09 Feb 2012 13:05:51 +0000] rev 287
more on the specification section
urbanc [Wed, 08 Feb 2012 16:35:49 +0000] rev 286
corrections by Xingyuan
urbanc [Tue, 07 Feb 2012 01:10:34 +0000] rev 285
more on paper
urbanc [Tue, 07 Feb 2012 00:50:23 +0000] rev 284
more on paper
urbanc [Mon, 06 Feb 2012 12:08:35 +0000] rev 283
paper updatated
urbanc [Sun, 05 Feb 2012 21:00:12 +0000] rev 282
moved unused theories to Attic
zhang [Sun, 05 Feb 2012 14:29:08 +0000] rev 281
README added.
urbanc [Sat, 04 Feb 2012 22:56:14 +0000] rev 280
updated
urbanc [Sat, 04 Feb 2012 00:14:41 +0000] rev 279
slight polishing
urbanc [Fri, 03 Feb 2012 11:26:11 +0000] rev 278
a bit more on the introduction
urbanc [Thu, 02 Feb 2012 13:58:16 +0000] rev 277
slight tuning
urbanc [Wed, 01 Feb 2012 17:46:36 +0000] rev 276
more on intro
urbanc [Wed, 01 Feb 2012 17:40:00 +0000] rev 275
more on intro
urbanc [Wed, 01 Feb 2012 15:00:17 +0000] rev 274
more on intro
urbanc [Wed, 01 Feb 2012 12:00:37 +0000] rev 273
slightly more on text
zhang [Wed, 01 Feb 2012 08:16:00 +0000] rev 272
All comments added.
urbanc [Mon, 30 Jan 2012 09:44:33 +0000] rev 271
spell check
urbanc [Mon, 30 Jan 2012 09:33:39 +0000] rev 270
slight polishing
urbanc [Mon, 30 Jan 2012 08:55:27 +0000] rev 269
more text
urbanc [Mon, 30 Jan 2012 08:45:56 +0000] rev 268
more text
urbanc [Mon, 30 Jan 2012 06:46:47 +0000] rev 267
added two paragraphs to the introduction
zhang [Sun, 29 Jan 2012 09:31:03 +0000] rev 266
More explanations added by XY.
urbanc [Fri, 27 Jan 2012 23:19:10 +0000] rev 265
changed abstract, intro and IsaMakefile
zhang [Fri, 27 Jan 2012 13:50:02 +0000] rev 264
Newer version.
urbanc [Tue, 24 Jan 2012 00:34:52 +0000] rev 263
minor edit
urbanc [Tue, 24 Jan 2012 00:20:09 +0000] rev 262
initial version of the PIP formalisation
urbanc [Mon, 26 Dec 2011 08:21:00 +0000] rev 261
changed to 11 months
urbanc [Thu, 22 Dec 2011 14:25:34 +0000] rev 260
added a draft of the letter for Chunhan
urbanc [Sat, 17 Dec 2011 13:32:11 +0000] rev 259
updated urls to AFP
urbanc [Sun, 20 Nov 2011 22:53:50 +0000] rev 258
added slides for a talk in St Andrews
urbanc [Fri, 11 Nov 2011 23:38:10 +0000] rev 257
small change
urbanc [Thu, 15 Sep 2011 12:46:00 +0000] rev 256
set -> language
urbanc [Wed, 14 Sep 2011 21:14:50 +0000] rev 255
added a paper about applications
urbanc [Wed, 14 Sep 2011 15:56:03 +0000] rev 254
added paper that recently appeared about rexps and pegs
urbanc [Wed, 14 Sep 2011 13:39:03 +0000] rev 253
polished the non-regularity proof
urbanc [Wed, 14 Sep 2011 13:00:44 +0000] rev 252
clarified proof about non-regularity
urbanc [Wed, 14 Sep 2011 11:46:50 +0000] rev 251
corrected typo found by Xingyuan
urbanc [Tue, 13 Sep 2011 12:00:53 +0000] rev 250
small typo
urbanc [Mon, 12 Sep 2011 19:50:21 +0000] rev 249
a final polishing before submitting later this week
urbanc [Thu, 08 Sep 2011 15:08:02 +0000] rev 248
one more itteration on the paper
urbanc [Wed, 07 Sep 2011 18:17:56 +0000] rev 247
some more polishing and a link to Haines
urbanc [Wed, 07 Sep 2011 18:16:49 +0000] rev 246
typos
urbanc [Wed, 07 Sep 2011 09:28:13 +0000] rev 245
polished a bit the journal paper
urbanc [Tue, 06 Sep 2011 02:52:26 +0000] rev 244
typo
urbanc [Tue, 06 Sep 2011 02:48:51 +0000] rev 243
more tuning on the proposal
urbanc [Tue, 06 Sep 2011 02:35:10 +0000] rev 242
polished proposal
urbanc [Mon, 05 Sep 2011 20:59:50 +0000] rev 241
tuning on the derivatives and closures theories
urbanc [Mon, 05 Sep 2011 15:42:29 +0000] rev 240
added section about non-regularity
urbanc [Mon, 05 Sep 2011 14:15:32 +0000] rev 239
polished SUBSEQ
urbanc [Mon, 05 Sep 2011 13:44:01 +0000] rev 238
slight polishing to SUBSEQ
urbanc [Mon, 05 Sep 2011 13:43:12 +0000] rev 237
slight polishing to SUBSEQ
urbanc [Mon, 05 Sep 2011 13:09:38 +0000] rev 236
shortened
urbanc [Mon, 05 Sep 2011 12:40:22 +0000] rev 235
some changes
urbanc [Mon, 05 Sep 2011 12:33:26 +0000] rev 234
some changes
urbanc [Mon, 05 Sep 2011 12:07:16 +0000] rev 233
added section about SUBSEQ and SUPSEQ
zhang [Sun, 04 Sep 2011 07:28:48 +0000] rev 232
Proposal paragraphs by Xingyuan completed (with references added).
urbanc [Sun, 04 Sep 2011 00:21:41 +0000] rev 231
removed the last two sorry's
zhang [Fri, 02 Sep 2011 14:29:54 +0000] rev 230
More modification by Xingyuan.
zhang [Fri, 02 Sep 2011 14:11:36 +0000] rev 229
One passage added.
urbanc [Fri, 02 Sep 2011 14:01:11 +0000] rev 228
latest changes
urbanc [Fri, 02 Sep 2011 13:34:45 +0000] rev 227
small change
urbanc [Fri, 02 Sep 2011 13:30:17 +0000] rev 226
small improvement
urbanc [Fri, 02 Sep 2011 13:29:46 +0000] rev 225
added a start for a proposal
urbanc [Fri, 02 Sep 2011 12:19:00 +0000] rev 224
added example about non-regularity
urbanc [Fri, 02 Sep 2011 09:53:56 +0000] rev 223
cleaned up proofs
urbanc [Thu, 01 Sep 2011 23:18:34 +0000] rev 222
included Higman's lemma from the Isabelle repository
urbanc [Thu, 01 Sep 2011 20:26:30 +0000] rev 221
solved the SUBSEQ/SUPSEQ problem
urbanc [Tue, 30 Aug 2011 11:31:18 +0000] rev 220
added a further test
urbanc [Fri, 26 Aug 2011 17:29:07 +0000] rev 219
corrected typo
urbanc [Fri, 26 Aug 2011 17:23:46 +0000] rev 218
added a few points
urbanc [Thu, 25 Aug 2011 19:33:41 +0000] rev 217
a few bits on the journal paper
urbanc [Thu, 25 Aug 2011 06:19:42 +0000] rev 216
shown slides
urbanc [Thu, 25 Aug 2011 06:18:58 +0000] rev 215
final polishing
urbanc [Wed, 24 Aug 2011 22:21:37 +0000] rev 214
added pdf of slides
urbanc [Wed, 24 Aug 2011 22:18:54 +0000] rev 213
final slides
urbanc [Wed, 24 Aug 2011 10:01:24 +0000] rev 212
more slides
urbanc [Wed, 24 Aug 2011 08:03:42 +0000] rev 211
more on slides
urbanc [Wed, 24 Aug 2011 07:24:22 +0000] rev 210
just test
urbanc [Tue, 23 Aug 2011 12:36:43 +0000] rev 209
added test for Higman's lemma
urbanc [Tue, 23 Aug 2011 11:53:25 +0000] rev 208
more on slides
urbanc [Tue, 23 Aug 2011 08:42:51 +0000] rev 207
more on the slides
urbanc [Tue, 23 Aug 2011 08:11:25 +0000] rev 206
more on the slides
urbanc [Tue, 23 Aug 2011 00:33:12 +0000] rev 205
forgotten file
urbanc [Tue, 23 Aug 2011 00:24:10 +0000] rev 204
beginnig of the slides (not yet finished)
urbanc [Mon, 22 Aug 2011 12:49:27 +0000] rev 203
changes according to afp-submission
urbanc [Fri, 19 Aug 2011 20:39:07 +0000] rev 202
two more literature
urbanc [Fri, 19 Aug 2011 06:57:57 +0000] rev 201
added comments by Xingyuan
urbanc [Wed, 17 Aug 2011 17:36:19 +0000] rev 200
added an example for non-regularity and continuation lemma (the example does not yet work)
urbanc [Wed, 17 Aug 2011 07:43:09 +0000] rev 199
a little tuning
urbanc [Tue, 16 Aug 2011 10:21:14 +0000] rev 198
final(?) version of the paper
urbanc [Mon, 15 Aug 2011 22:36:26 +0000] rev 197
a bit more polishing
urbanc [Mon, 15 Aug 2011 21:09:08 +0000] rev 196
polishing of the closure section and conclusion
urbanc [Fri, 12 Aug 2011 17:08:58 +0000] rev 195
small typo
urbanc [Thu, 11 Aug 2011 23:42:06 +0000] rev 194
some typos
urbanc [Thu, 11 Aug 2011 23:11:39 +0000] rev 193
finished section about derivatives and closure properties
urbanc [Thu, 11 Aug 2011 16:55:41 +0000] rev 192
two interesting papers
urbanc [Thu, 11 Aug 2011 10:26:19 +0000] rev 191
slight polishing
urbanc [Tue, 09 Aug 2011 22:15:11 +0000] rev 190
more on paper
urbanc [Tue, 09 Aug 2011 22:14:41 +0000] rev 189
more on paper and literature
urbanc [Fri, 05 Aug 2011 15:38:28 +0000] rev 188
added paper on partial derivatives
urbanc [Fri, 05 Aug 2011 05:34:11 +0000] rev 187
more on the derivatives section
urbanc [Wed, 03 Aug 2011 17:08:31 +0000] rev 186
added more to the derivatives section
urbanc [Wed, 03 Aug 2011 13:56:01 +0000] rev 185
completed the taging-function section
urbanc [Wed, 03 Aug 2011 12:36:23 +0000] rev 184
more on the paper
urbanc [Wed, 03 Aug 2011 00:52:41 +0000] rev 183
cleaned up the proofs in Myhill_2
urbanc [Tue, 02 Aug 2011 15:27:37 +0000] rev 182
a version of the proof which dispenses with the notion of string-subtraction
urbanc [Sun, 31 Jul 2011 10:27:41 +0000] rev 181
some experiments with the proofs in Myhill_2
urbanc [Thu, 28 Jul 2011 17:52:36 +0000] rev 180
added a picture
urbanc [Thu, 28 Jul 2011 14:22:10 +0000] rev 179
small improvements
urbanc [Thu, 28 Jul 2011 11:56:25 +0000] rev 178
added more examles
urbanc [Thu, 28 Jul 2011 01:12:02 +0000] rev 177
more one the paper
urbanc [Wed, 27 Jul 2011 15:29:39 +0000] rev 176
latest version of the journal paper
urbanc [Wed, 27 Jul 2011 12:32:28 +0000] rev 175
polished the introduction
urbanc [Tue, 26 Jul 2011 18:12:07 +0000] rev 174
more on the section about derivatives
urbanc [Tue, 26 Jul 2011 10:58:26 +0000] rev 173
more on the introduction of the journal paper
urbanc [Mon, 25 Jul 2011 18:00:52 +0000] rev 172
more on the journal paper
urbanc [Mon, 25 Jul 2011 15:40:12 +0000] rev 171
added a paper about PEG-parsing and left recursion
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
zhang [Fri, 03 Jun 2011 13:59:21 +0000] rev 169
added boolean grammar
zhang [Fri, 03 Jun 2011 13:54:14 +0000] rev 168
added
urbanc [Thu, 02 Jun 2011 20:02:16 +0000] rev 167
added a journal version
urbanc [Thu, 02 Jun 2011 16:44:35 +0000] rev 166
updated theories and itp-paper
urbanc [Tue, 31 May 2011 20:32:49 +0000] rev 165
added missing file
urbanc [Sun, 29 May 2011 20:01:37 +0000] rev 164
added old paper
urbanc [Thu, 26 May 2011 18:39:36 +0000] rev 163
a few more literature places
urbanc [Wed, 18 May 2011 19:54:43 +0000] rev 162
added directory for journal version; took uptodate version of the theory files
urbanc [Thu, 12 May 2011 05:55:05 +0000] rev 161
preparation for final paper version
urbanc [Mon, 09 May 2011 07:25:37 +0000] rev 160
added comments from Chunhan
urbanc [Wed, 04 May 2011 07:05:59 +0000] rev 159
edits; sqeezed to 16 pages
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
urbanc [Thu, 21 Apr 2011 22:41:15 +0000] rev 157
a small change
urbanc [Thu, 21 Apr 2011 12:07:11 +0000] rev 156
a few more changes
urbanc [Tue, 19 Apr 2011 02:25:21 +0000] rev 155
removed experimental code from Matcher
urbanc [Tue, 19 Apr 2011 02:19:56 +0000] rev 154
implemented most suggestions from the reviewers
urbanc [Wed, 06 Apr 2011 08:18:23 +0000] rev 153
added literature about parsing
urbanc [Fri, 25 Mar 2011 09:42:33 +0000] rev 152
MN via partial derivatives
urbanc [Wed, 23 Mar 2011 13:33:55 +0000] rev 151
moved paper to correct place
urbanc [Wed, 23 Mar 2011 12:22:54 +0000] rev 150
added paper by Antimirov
urbanc [Wed, 23 Mar 2011 12:17:30 +0000] rev 149
added the most current versions of the theories.
urbanc [Tue, 15 Mar 2011 15:53:22 +0000] rev 148
correct version
urbanc [Tue, 15 Mar 2011 15:52:44 +0000] rev 147
deleted wrong version
urbanc [Tue, 15 Mar 2011 14:29:41 +0000] rev 146
added chapter about regular expressions by Sakarovitch (interesting pages are 139 - 142)
urbanc [Tue, 15 Mar 2011 11:04:53 +0000] rev 145
corrected small typo
urbanc [Sat, 05 Mar 2011 11:42:14 +0000] rev 144
slight polishing of the bibliography
urbanc [Sat, 05 Mar 2011 11:06:39 +0000] rev 143
formalisation of first direction is now only 780 loc
urbanc [Sat, 26 Feb 2011 15:44:38 +0000] rev 142
changed one occurence of tagging function into tagging relation
urbanc [Fri, 25 Feb 2011 12:41:35 +0000] rev 141
added yacc is dead paper
urbanc [Thu, 24 Feb 2011 00:37:46 +0000] rev 140
added a paper about derivatives
urbanc [Thu, 24 Feb 2011 00:34:45 +0000] rev 139
added hocroft and ullman book
urbanc [Tue, 22 Feb 2011 12:43:05 +0000] rev 138
three typos
urbanc [Mon, 21 Feb 2011 03:35:39 +0000] rev 137
one further polishing
urbanc [Mon, 21 Feb 2011 03:33:27 +0000] rev 136
final final polishing
urbanc [Mon, 21 Feb 2011 03:30:38 +0000] rev 135
final polished
urbanc [Mon, 21 Feb 2011 02:33:05 +0000] rev 134
chunhan's comments
urbanc [Sun, 20 Feb 2011 18:58:34 +0000] rev 133
minor change
urbanc [Sun, 20 Feb 2011 18:54:31 +0000] rev 132
comments by Xingyuan
urbanc [Sun, 20 Feb 2011 17:47:54 +0000] rev 131
chunhan's comments
urbanc [Sun, 20 Feb 2011 13:43:00 +0000] rev 130
pre-final version
urbanc [Sun, 20 Feb 2011 12:52:35 +0000] rev 129
minor
urbanc [Sun, 20 Feb 2011 12:51:04 +0000] rev 128
finished picture
urbanc [Sun, 20 Feb 2011 11:14:07 +0000] rev 127
seq case finished
urbanc [Sun, 20 Feb 2011 09:54:24 +0000] rev 126
latest update
urbanc [Sun, 20 Feb 2011 08:12:13 +0000] rev 125
added pictures for seq-case
urbanc [Sun, 20 Feb 2011 07:33:54 +0000] rev 124
added definition of string prefix and string subtraction
urbanc [Sun, 20 Feb 2011 06:02:58 +0000] rev 123
polished everywhere...two cases still missing
urbanc [Sat, 19 Feb 2011 22:05:22 +0000] rev 122
my latest version (SEQ and STAR still missing)
urbanc [Sat, 19 Feb 2011 21:49:11 +0000] rev 121
added directory with the small files and numbers of lines
urbanc [Sat, 19 Feb 2011 20:15:59 +0000] rev 120
ALT case done
urbanc [Sat, 19 Feb 2011 19:27:33 +0000] rev 119
first two proofs in 2 direction
urbanc [Sat, 19 Feb 2011 17:10:46 +0000] rev 118
first proof
urbanc [Sat, 19 Feb 2011 12:01:16 +0000] rev 117
updated second direction
urbanc [Sat, 19 Feb 2011 10:23:51 +0000] rev 116
included comments by Chunhan
urbanc [Fri, 18 Feb 2011 15:06:06 +0000] rev 115
added comment from Larry
urbanc [Fri, 18 Feb 2011 14:26:23 +0000] rev 114
updated bib
urbanc [Fri, 18 Feb 2011 12:14:07 +0000] rev 113
polished everything
urbanc [Thu, 17 Feb 2011 21:30:26 +0000] rev 112
more on the conclusion
urbanc [Thu, 17 Feb 2011 13:25:29 +0000] rev 111
first ideas about conclusion
urbanc [Thu, 17 Feb 2011 11:42:16 +0000] rev 110
completed first direction
urbanc [Wed, 16 Feb 2011 12:25:53 +0000] rev 109
minor updated
urbanc [Wed, 16 Feb 2011 06:51:58 +0000] rev 108
filled details in one place
urbanc [Tue, 15 Feb 2011 14:17:31 +0000] rev 107
updated paper
urbanc [Tue, 15 Feb 2011 12:01:29 +0000] rev 106
updated paper
urbanc [Tue, 15 Feb 2011 10:37:56 +0000] rev 105
updated paper
urbanc [Tue, 15 Feb 2011 08:08:04 +0000] rev 104
updated paper
urbanc [Mon, 14 Feb 2011 23:10:44 +0000] rev 103
updated
urbanc [Mon, 14 Feb 2011 11:12:01 +0000] rev 102
added definition of DERIV and delta
urbanc [Mon, 14 Feb 2011 09:38:18 +0000] rev 101
updated paper
urbanc [Mon, 14 Feb 2011 07:42:16 +0000] rev 100
updated
zhang [Sun, 13 Feb 2011 10:36:53 +0000] rev 99
More into the second direction
urbanc [Fri, 11 Feb 2011 13:30:37 +0000] rev 98
included comments by Xingyuan
urbanc [Fri, 11 Feb 2011 12:13:35 +0000] rev 97
slightly streamlined the proof
urbanc [Thu, 10 Feb 2011 21:00:40 +0000] rev 96
simplified a bit the proof
urbanc [Thu, 10 Feb 2011 13:10:16 +0000] rev 95
more things
urbanc [Thu, 10 Feb 2011 12:32:45 +0000] rev 94
latest on the paper
urbanc [Thu, 10 Feb 2011 08:40:38 +0000] rev 93
more on the paper
urbanc [Thu, 10 Feb 2011 05:57:56 +0000] rev 92
more on paper
urbanc [Wed, 09 Feb 2011 12:34:30 +0000] rev 91
added Xingyuan's changes with the while combinator
urbanc [Wed, 09 Feb 2011 09:46:59 +0000] rev 90
added an example
urbanc [Wed, 09 Feb 2011 07:27:30 +0000] rev 89
a bit more on the paper
urbanc [Wed, 09 Feb 2011 06:09:46 +0000] rev 88
added something about Setalt and folds
urbanc [Wed, 09 Feb 2011 04:54:23 +0000] rev 87
deleted the non_empty invariant
urbanc [Wed, 09 Feb 2011 04:50:18 +0000] rev 86
tuned comments and names in Myhill_1
urbanc [Wed, 09 Feb 2011 03:52:28 +0000] rev 85
separated the definition of folds into a separate file
urbanc [Wed, 09 Feb 2011 03:33:30 +0000] rev 84
saved a copy of the current Myhill for reference
urbanc [Tue, 08 Feb 2011 19:54:23 +0000] rev 83
a bit more on the paper
urbanc [Tue, 08 Feb 2011 18:04:54 +0000] rev 82
added coments about functions
urbanc [Tue, 08 Feb 2011 16:49:18 +0000] rev 81
more direct definitions
urbanc [Tue, 08 Feb 2011 15:59:47 +0000] rev 80
deleted lam_of
urbanc [Tue, 08 Feb 2011 15:50:26 +0000] rev 79
started to define things more directly
zhang [Tue, 08 Feb 2011 12:01:28 +0000] rev 78
More explaination on equational system
urbanc [Tue, 08 Feb 2011 09:51:49 +0000] rev 77
small additions
urbanc [Tue, 08 Feb 2011 09:51:27 +0000] rev 76
added an abbreviation for folds ALT NULL
urbanc [Mon, 07 Feb 2011 20:30:10 +0000] rev 75
parts of the 3 section
urbanc [Mon, 07 Feb 2011 13:17:01 +0000] rev 74
added bib-file
zhang [Mon, 07 Feb 2011 13:08:09 +0000] rev 73
More into first direction
urbanc [Mon, 07 Feb 2011 11:12:36 +0000] rev 72
added an option fullpaper to IsaMakefile
urbanc [Mon, 07 Feb 2011 10:23:23 +0000] rev 71
more on the paper
urbanc [Sun, 06 Feb 2011 11:21:12 +0000] rev 70
slightly more on the paper
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
zhang [Sat, 05 Feb 2011 13:56:50 +0000] rev 68
Check in Myhill.thy before trying another way to explain DFA
urbanc [Sat, 05 Feb 2011 09:54:52 +0000] rev 67
more intro
urbanc [Fri, 04 Feb 2011 22:54:29 +0000] rev 66
more on the introduction
urbanc [Fri, 04 Feb 2011 13:33:18 +0000] rev 65
exercise about arden from TU Munich
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.
zhang [Thu, 03 Feb 2011 12:44:46 +0000] rev 63
Myhill_2.thy added
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.
urbanc [Thu, 03 Feb 2011 09:54:19 +0000] rev 61
more to the intro
urbanc [Thu, 03 Feb 2011 05:38:47 +0000] rev 60
a bit more tuning on the introduction
urbanc [Wed, 02 Feb 2011 15:43:22 +0000] rev 59
more on the intro
urbanc [Wed, 02 Feb 2011 13:54:07 +0000] rev 58
a little bit in the introduction
zhang [Wed, 02 Feb 2011 13:25:09 +0000] rev 57
Myhill.pdf modified
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
zhang [Mon, 31 Jan 2011 14:51:47 +0000] rev 55
Myhill.thy IsabelleMakefile modified
urbanc [Mon, 31 Jan 2011 12:54:31 +0000] rev 54
a bit more on the paper
urbanc [Sun, 30 Jan 2011 17:24:37 +0000] rev 53
small typo
urbanc [Sun, 30 Jan 2011 17:21:53 +0000] rev 52
tuning of the syntax; needs the stmaryrd latex package
urbanc [Sun, 30 Jan 2011 17:09:02 +0000] rev 51
some tuning of the paper
urbanc [Sun, 30 Jan 2011 16:59:57 +0000] rev 50
revised proof of Ardens lemma
zhang [Sun, 30 Jan 2011 12:22:07 +0000] rev 49
Illustration added together with renewed explainations for case STAR.
zhang [Sat, 29 Jan 2011 11:41:17 +0000] rev 48
Myhill.thy and Myhill_1.thy changed.
urbanc [Fri, 28 Jan 2011 19:17:40 +0000] rev 47
slightly tuned the main lemma and the finiteness proofs
wu [Fri, 28 Jan 2011 12:53:01 +0000] rev 46
test
zhang [Fri, 28 Jan 2011 11:52:11 +0000] rev 45
More improvement
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].
wu [Fri, 07 Jan 2011 14:25:23 +0000] rev 29
Beautifying of the Other Direction is finished.
wu [Fri, 31 Dec 2010 13:47:53 +0000] rev 28
Rewritten of hard direction once more. To make it looking better.
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.
urbanc [Fri, 26 Nov 2010 12:34:34 +0000] rev 26
added a recent paper by Tobias Nipkow on regular expressions
urbanc [Fri, 26 Nov 2010 10:53:14 +0000] rev 25
added interesting paper by rutten
urbanc [Thu, 25 Nov 2010 18:54:45 +0000] rev 24
added paper
wu [Thu, 18 Nov 2010 11:39:17 +0000] rev 23
All cases of the Other direction finished
urbanc [Wed, 10 Nov 2010 11:59:29 +0000] rev 22
added a test file
urbanc [Wed, 10 Nov 2010 11:53:07 +0000] rev 21
my slides from the talk in Cambridge
urbanc [Wed, 10 Nov 2010 11:49:45 +0000] rev 20
added my slides
urbanc [Mon, 08 Nov 2010 01:13:09 +0000] rev 19
slight tuning of proof by Chunhan
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.
urbanc [Wed, 03 Nov 2010 22:08:50 +0000] rev 17
added more experiments
urbanc [Wed, 03 Nov 2010 21:42:44 +0000] rev 16
added initial slides for informal talk in Cambridge
urbanc [Tue, 26 Oct 2010 23:09:31 +0000] rev 15
added slides of chunhan
urbanc [Tue, 26 Oct 2010 13:01:22 +0000] rev 14
more experiments
urbanc [Sun, 24 Oct 2010 01:17:44 +0000] rev 13
a few more experiments, but no proof for the ALT-case
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
urbanc [Fri, 22 Oct 2010 19:43:56 +0000] rev 11
deleted two unnecessary lemmas
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
urbanc [Thu, 21 Oct 2010 15:35:03 +0000] rev 9
deleted the test
urbanc [Thu, 21 Oct 2010 15:06:30 +0000] rev 8
tried at the end to prove the other direction (failed at the moment)
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
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
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)
wu [Thu, 07 Oct 2010 05:30:21 +0000] rev 4
Add a test file, after testing, this file can be deleted.
chunhan, 2010-10-7, in nanjing
urbanc [Sun, 03 Oct 2010 08:12:48 +0000] rev 3
added simple regexp matcher from Slind et al
urbanc [Sun, 03 Oct 2010 06:55:21 +0000] rev 2
test
urbanc [Sun, 03 Oct 2010 06:42:01 +0000] rev 1
added literature
urbanc [Sun, 03 Oct 2010 06:32:12 +0000] rev 0
added initial version by Chunhan