| 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 |