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.