src/HOL/ex/Tree23.thy
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
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