src/HOL/ex/Tree23.thy
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-04 huffman 2011-11-04 ex/Tree23.thy: automate proof of gfull_add
2011-11-04 huffman 2011-11-04 ex/Tree23.thy: simplify proof of bal_del0
2011-11-04 huffman 2011-11-04 ex/Tree23.thy: simplify proof of bal_add0
2011-11-04 huffman 2011-11-04 ex/Tree23.thy: simpler definition of ordered-ness predicate
2011-11-03 huffman 2011-11-03 ex/Tree23.thy: prove that deletion preserves balance
2011-11-03 huffman 2011-11-03 ex/Tree23.thy: prove that insertion preserves tree balance and order
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2009-11-04 nipkow 2009-11-04 New