| Sun, 15 Jan 2023 18:30:18 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2020 17:42:41 +0100 |
nipkow |
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
|
file |
diff |
annotate
|
| 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
|