src/HOL/Library/Tree.thy
16 months ago nipkow 2018-05-08 new def of sorted and sorted_wrt
20 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
24 months ago nipkow 2017-09-17 added lemmas
2017-09-05 nipkow 2017-09-05 introduced bst_wrt
2017-04-01 nipkow 2017-04-01 tuned
2017-03-31 nipkow 2017-03-31 more lemmas
2017-01-20 nipkow 2017-01-20 added postorder
2017-01-20 nipkow 2017-01-20 tuned
2017-01-19 nipkow 2017-01-19 int version slicker
2017-01-19 nipkow 2017-01-19 tuned
2017-01-18 nipkow 2017-01-18 tuned
2017-01-17 nipkow 2017-01-17 tuned
2017-01-13 nipkow 2017-01-13 tuned/minimized
2017-01-04 nipkow 2017-01-04 tuned
2016-12-05 nipkow 2016-12-05 spelling
2016-11-29 nipkow 2016-11-29 more lemmas, tuned proofs
2016-10-27 nipkow 2016-10-27 added lemma
2016-09-13 nipkow 2016-09-13 reorganization, more funs and lemmas
2016-09-09 nipkow 2016-09-09 More on balancing; renamed theory to Balance
2016-09-02 nipkow 2016-09-02 added lemmas
2016-09-02 nipkow 2016-09-02 added inorder2
2016-09-01 nipkow 2016-09-01 Renamed balanced to complete; added balanced; more about both
2016-08-12 nipkow 2016-08-12 added lemma
2016-08-05 nipkow 2016-08-05 added min_height
2016-07-08 nipkow 2016-07-08 added path_len
2016-04-22 nipkow 2016-04-22 added "balanced" predicate
2016-03-18 nipkow 2016-03-18 added tree lemmas
2016-01-19 nipkow 2016-01-19 added lemma
2016-01-13 nipkow 2016-01-13 tuned layout
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-07-28 nipkow 2015-07-28 depth -> height; removed del_rightmost (too specifi)
2015-06-17 nipkow 2015-06-17 tuned
2015-06-17 nipkow 2015-06-17 merged
2015-06-17 nipkow 2015-06-17 added funs and lemmas
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-04-06 nipkow 2015-04-06 new theory Library/Tree_Multiset.thy
2015-03-23 nipkow 2015-03-23 added funs and lemmas
2015-02-21 nipkow 2015-02-21 added new tree material
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-28 haftmann 2014-09-28 moved to HOL and generalized
2014-09-25 nipkow 2014-09-25 added function size1
2014-09-24 nipkow 2014-09-24 added nice standard syntax
2014-09-11 blanchet 2014-09-11 updated news
2014-07-25 nipkow 2014-07-25 added more functions and lemmas
2014-07-17 hoelzl 2014-07-17 register tree with datatype_compat ot support QuickCheck
2014-07-07 nipkow 2014-07-07 added lemma
2014-07-01 hoelzl 2014-07-01 Library/Tree: bst is preferred to be a function
2014-07-01 hoelzl 2014-07-01 Library/Tree: use datatype_new, bst is an inductive predicate
2014-06-12 nipkow 2014-06-12 new theory of binary trees
2010-02-18 haftmann 2010-02-18 drop code lemma for ordered_keys
2010-02-17 haftmann 2010-02-17 adjusted to changes in theory Mapping
2009-06-04 haftmann 2009-06-04 added trees implementing mappings