2011-08-22 |
urbanc |
changes according to afp-submission
|
file |
diff |
annotate
|
2011-07-31 |
urbanc |
some experiments with the proofs in Myhill_2
|
file |
diff |
annotate
|
2011-07-28 |
urbanc |
small improvements
|
file |
diff |
annotate
|
2011-07-25 |
urbanc |
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
|
file |
diff |
annotate
|
2011-06-02 |
urbanc |
updated theories and itp-paper
|
file |
diff |
annotate
|
2011-05-18 |
urbanc |
added directory for journal version; took uptodate version of the theory files
|
file |
diff |
annotate
|
2011-03-23 |
urbanc |
added the most current versions of the theories.
|
file |
diff |
annotate
|
2011-02-17 |
urbanc |
completed first direction
|
file |
diff |
annotate
|
2011-02-16 |
urbanc |
minor updated
|
file |
diff |
annotate
|
2011-02-16 |
urbanc |
filled details in one place
|
file |
diff |
annotate
|
2011-02-15 |
urbanc |
updated paper
|
file |
diff |
annotate
|
2011-02-15 |
urbanc |
updated paper
|
file |
diff |
annotate
|
2011-02-15 |
urbanc |
updated paper
|
file |
diff |
annotate
|
2011-02-14 |
urbanc |
updated
|
file |
diff |
annotate
|
2011-02-14 |
urbanc |
updated paper
|
file |
diff |
annotate
|
2011-02-14 |
urbanc |
updated
|
file |
diff |
annotate
|
2011-02-13 |
zhang |
More into the second direction
|
file |
diff |
annotate
|
2011-02-11 |
urbanc |
included comments by Xingyuan
|
file |
diff |
annotate
|
2011-02-11 |
urbanc |
slightly streamlined the proof
|
file |
diff |
annotate
|
2011-02-10 |
urbanc |
simplified a bit the proof
|
file |
diff |
annotate
|
2011-02-10 |
urbanc |
more things
|
file |
diff |
annotate
|
2011-02-10 |
urbanc |
latest on the paper
|
file |
diff |
annotate
|
2011-02-10 |
urbanc |
more on paper
|
file |
diff |
annotate
|
2011-02-09 |
urbanc |
added Xingyuan's changes with the while combinator
|
file |
diff |
annotate
|
2011-02-09 |
urbanc |
a bit more on the paper
|
file |
diff |
annotate
|
2011-02-09 |
urbanc |
added something about Setalt and folds
|
file |
diff |
annotate
|
2011-02-09 |
urbanc |
deleted the non_empty invariant
|
file |
diff |
annotate
|
2011-02-09 |
urbanc |
tuned comments and names in Myhill_1
|
file |
diff |
annotate
|
2011-02-08 |
urbanc |
more direct definitions
|
file |
diff |
annotate
|
2011-02-08 |
urbanc |
deleted lam_of
|
file |
diff |
annotate
|
2011-02-08 |
urbanc |
started to define things more directly
|
file |
diff |
annotate
|
2011-02-08 |
urbanc |
added an abbreviation for folds ALT NULL
|
file |
diff |
annotate
|
2011-02-07 |
urbanc |
parts of the 3 section
|
file |
diff |
annotate
|
2011-02-07 |
urbanc |
more on the paper
|
file |
diff |
annotate
|
2011-02-06 |
urbanc |
slightly more on the paper
|
file |
diff |
annotate
|
2011-02-04 |
urbanc |
more on the introduction
|
file |
diff |
annotate
|
2011-02-03 |
urbanc |
a bit more tuning on the introduction
|
file |
diff |
annotate
|
2011-02-02 |
urbanc |
removed the inductive definition of Star and replaced it by a definition in terms of pow
|
file |
diff |
annotate
|
2011-01-31 |
urbanc |
a bit more on the paper
|
file |
diff |
annotate
|
2011-01-30 |
urbanc |
revised proof of Ardens lemma
|
file |
diff |
annotate
|
2011-01-29 |
zhang |
Myhill.thy and Myhill_1.thy changed.
|
file |
diff |
annotate
|
2011-01-28 |
wu |
test
|
file |
diff |
annotate
|
2011-01-27 |
urbanc |
added my changes again
|
file |
diff |
annotate
|
2011-01-27 |
zhang |
Trying to solve the confict
|
file |
diff |
annotate
|