| Tue, 10 Nov 2020 17:42:41 +0100 |
nipkow |
renamed "balanced" -> "acomplete" because balanced has other meanings in the literature
|
file |
diff |
annotate
|
| Sun, 24 May 2020 08:20:05 +0200 |
nipkow |
simpler inductions
|
file |
diff |
annotate
|
| Tue, 19 May 2020 09:33:16 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 24 Sep 2019 16:10:27 +0200 |
nipkow |
simplified proofs
|
file |
diff |
annotate
|
| Mon, 23 Sep 2019 17:15:29 +0200 |
nipkow |
Enforced precodition "n <= length xs" to avoid relying on "hd []".
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 17:52:00 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 16:47:25 +0200 |
nipkow |
reorganized and added log-related lemmas
|
file |
diff |
annotate
|
| Fri, 25 Aug 2017 23:09:56 +0200 |
nipkow |
reorganization of tree lemmas; new lemmas
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Wed, 07 Dec 2016 08:14:40 +0100 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| Mon, 05 Dec 2016 18:14:41 +0100 |
nipkow |
spelling
|
file |
diff |
annotate
|
| Tue, 29 Nov 2016 10:53:52 +0100 |
nipkow |
more lemmas, tuned proofs
|
file |
diff |
annotate
|
| Tue, 08 Nov 2016 13:03:54 +0100 |
nipkow |
provided more efficient interface
|
file |
diff |
annotate
|
| Thu, 06 Oct 2016 11:38:05 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Wed, 05 Oct 2016 20:01:05 +0200 |
nipkow |
replaced floorlog by floor/ceiling(log .)
|
file |
diff |
annotate
|
| Tue, 13 Sep 2016 11:31:30 +0200 |
nipkow |
reorganization, more funs and lemmas
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 18:12:05 +0200 |
nipkow |
more simp rules
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 14:15:16 +0200 |
nipkow |
More on balancing; renamed theory to Balance
|
file |
diff |
annotate
| base
|