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