| Fri, 18 Mar 2016 10:14:56 +0100 | nipkow | added tree lemmas | file | diff | annotate |
| Tue, 19 Jan 2016 11:36:02 +0100 | nipkow | added lemma | file | diff | annotate |
| Wed, 13 Jan 2016 09:38:16 +0100 | nipkow | tuned layout | file | diff | annotate |
| Thu, 05 Nov 2015 10:39:49 +0100 | wenzelm | isabelle update_cartouches -c -t; | file | diff | annotate |
| Tue, 28 Jul 2015 13:00:54 +0200 | nipkow | depth -> height; removed del_rightmost (too specifi) | file | diff | annotate |
| Wed, 17 Jun 2015 22:06:56 +0200 | nipkow | tuned | file | diff | annotate |
| Wed, 17 Jun 2015 20:22:01 +0200 | nipkow | merged | file | diff | annotate |
| Wed, 17 Jun 2015 20:21:40 +0200 | nipkow | added funs and lemmas | file | diff | annotate |
| Wed, 17 Jun 2015 11:03:05 +0200 | wenzelm | isabelle update_cartouches; | file | diff | annotate |
| Mon, 06 Apr 2015 15:23:50 +0200 | nipkow | new theory Library/Tree_Multiset.thy | file | diff | annotate |
| Mon, 23 Mar 2015 07:36:27 +0100 | nipkow | added funs and lemmas | file | diff | annotate |
| Sat, 21 Feb 2015 23:22:13 +0100 | nipkow | added new tree material | file | diff | annotate |
| Sun, 02 Nov 2014 17:20:45 +0100 | wenzelm | modernized header; | file | diff | annotate |
| Sun, 28 Sep 2014 20:27:46 +0200 | haftmann | moved to HOL and generalized | file | diff | annotate |
| Thu, 25 Sep 2014 11:38:56 +0200 | nipkow | added function size1 | file | diff | annotate |
| Wed, 24 Sep 2014 11:09:05 +0200 | nipkow | added nice standard syntax | file | diff | annotate |
| Thu, 11 Sep 2014 19:32:36 +0200 | blanchet | updated news | file | diff | annotate |
| Fri, 25 Jul 2014 18:41:53 +0200 | nipkow | added more functions and lemmas | file | diff | annotate |
| Thu, 17 Jul 2014 14:55:56 +0200 | hoelzl | register tree with datatype_compat ot support QuickCheck | file | diff | annotate |
| Mon, 07 Jul 2014 17:01:11 +0200 | nipkow | added lemma | file | diff | annotate |
| Tue, 01 Jul 2014 15:57:07 +0200 | hoelzl | Library/Tree: bst is preferred to be a function | file | diff | annotate |
| Tue, 01 Jul 2014 15:25:27 +0200 | hoelzl | Library/Tree: use datatype_new, bst is an inductive predicate | file | diff | annotate |
| Thu, 12 Jun 2014 21:23:28 +0200 | nipkow | new theory of binary trees | file | diff | annotate |
| Thu, 18 Feb 2010 08:17:12 +0100 | haftmann | drop code lemma for ordered_keys | file | diff | annotate |
| Wed, 17 Feb 2010 09:48:53 +0100 | haftmann | adjusted to changes in theory Mapping | file | diff | annotate |
| Thu, 04 Jun 2009 16:55:20 +0200 | haftmann | added trees implementing mappings | file | diff | annotate |