| Mon, 14 Jan 2019 16:10:56 +0100 | nipkow | root_val -> value | file | diff | annotate |
| Fri, 04 Jan 2019 23:22:53 +0100 | wenzelm | isabelle update -u control_cartouches; | file | diff | annotate |
| Thu, 01 Nov 2018 12:23:54 +0100 | nipkow | too many clashes with "root" on reals | file | diff | annotate |
| Thu, 01 Nov 2018 11:26:38 +0100 | nipkow | added and renamed functions | file | diff | annotate |
| Thu, 04 Oct 2018 10:35:29 +0200 | nipkow | simplified proofs | file | diff | annotate |
| Wed, 03 Oct 2018 20:55:59 +0200 | nipkow | tuned | file | diff | annotate |
| Sun, 16 Sep 2018 16:31:56 +0200 | nipkow | tuned | file | diff | annotate |
| Sun, 16 Sep 2018 15:16:04 +0200 | nipkow | more traditional formulation | file | diff | annotate |
| Tue, 08 May 2018 10:14:36 +0200 | nipkow | new def of sorted and sorted_wrt | file | diff | annotate |
| Wed, 10 Jan 2018 15:25:09 +0100 | nipkow | ran isabelle update_op on all sources | file | diff | annotate |
| Sun, 17 Sep 2017 21:04:02 +0200 | nipkow | added lemmas | file | diff | annotate |
| Tue, 05 Sep 2017 17:07:42 +0200 | nipkow | introduced bst_wrt | file | diff | annotate |
| Sat, 01 Apr 2017 08:05:40 +0200 | nipkow | tuned | file | diff | annotate |
| Fri, 31 Mar 2017 17:21:36 +0200 | nipkow | more lemmas | file | diff | annotate |
| Fri, 20 Jan 2017 12:44:44 +0100 | nipkow | added postorder | file | diff | annotate |
| Fri, 20 Jan 2017 08:49:06 +0100 | nipkow | tuned | file | diff | annotate |
| Thu, 19 Jan 2017 17:24:05 +0100 | nipkow | int version slicker | file | diff | annotate |
| Thu, 19 Jan 2017 12:39:46 +0100 | nipkow | tuned | file | diff | annotate |
| Wed, 18 Jan 2017 21:03:39 +0100 | nipkow | tuned | file | diff | annotate |
| Tue, 17 Jan 2017 18:03:59 +0100 | nipkow | tuned | file | diff | annotate |
| Fri, 13 Jan 2017 11:41:50 +0100 | nipkow | tuned/minimized | file | diff | annotate |
| Wed, 04 Jan 2017 14:26:08 +0100 | nipkow | tuned | 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 |
| Thu, 27 Oct 2016 12:54:55 +0200 | nipkow | added lemma | file | diff | annotate |
| Tue, 13 Sep 2016 11:31:30 +0200 | nipkow | reorganization, more funs and lemmas | file | diff | annotate |
| Fri, 09 Sep 2016 14:15:16 +0200 | nipkow | More on balancing; renamed theory to Balance | file | diff | annotate |
| Fri, 02 Sep 2016 16:10:15 +0200 | nipkow | added lemmas | file | diff | annotate |
| Fri, 02 Sep 2016 08:34:26 +0200 | nipkow | added inorder2 | file | diff | annotate |
| Thu, 01 Sep 2016 15:57:54 +0200 | nipkow | Renamed balanced to complete; added balanced; more about both | file | diff | annotate |
| Fri, 12 Aug 2016 18:08:40 +0200 | nipkow | added lemma | file | diff | annotate |
| Fri, 05 Aug 2016 10:05:50 +0200 | nipkow | added min_height | file | diff | annotate |
| Fri, 08 Jul 2016 16:38:31 +0200 | nipkow | added path_len | file | diff | annotate |
| Fri, 22 Apr 2016 15:34:37 +0200 | nipkow | added "balanced" predicate | file | diff | annotate |
| 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 |