Tue, 17 Dec 2019 08:05:59 +0100 |
nipkow |
slicker proofs (used in CPP paper)
|
file |
diff |
annotate
|
Mon, 07 Oct 2019 14:31:46 +0200 |
nipkow |
simplified proof
|
file |
diff |
annotate
|
Sun, 30 Dec 2018 10:34:56 +0000 |
haftmann |
prefer naming convention from datatype package for strong congruence rules
|
file |
diff |
annotate
|
Sun, 28 Oct 2018 11:00:00 +0100 |
nipkow |
tuned names
|
file |
diff |
annotate
|
Sat, 27 Oct 2018 15:30:38 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
Fri, 26 Oct 2018 21:19:07 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Fri, 26 Oct 2018 21:07:30 +0200 |
nipkow |
tuned and added lemmas
|
file |
diff |
annotate
|
Fri, 26 Oct 2018 15:58:41 +0200 |
nipkow |
avoid abbreviation that is used only locally
|
file |
diff |
annotate
|
Fri, 26 Oct 2018 14:11:59 +0200 |
nipkow |
more combinatorics lemmas
|
file |
diff |
annotate
|
Wed, 17 Oct 2018 07:50:46 +0200 |
nipkow |
more intuitive and simpler (but slower) proofs
|
file |
diff |
annotate
|
Sun, 07 Oct 2018 16:28:38 +0200 |
nipkow |
added Braun_Tree.thy
|
file |
diff |
annotate
|