more abstract naming
tuned order of arguments
del_max -> split_max
more symbols;
isabelle update_cartouches -c;
replaced raw proof blocks by local lemmas
got rid of class cmp; added height-size proofs by Daniel Stuewe
added invariant proofs to AA trees
added AA_Map; tuned titles