src/HOL/Data_Structures/AA_Map.thy
2016-07-07 nipkow 2016-07-07 got rid of class cmp; added height-size proofs by Daniel Stuewe
2016-03-02 nipkow 2016-03-02 added invariant proofs to AA trees
2016-01-11 nipkow 2016-01-11 added AA_Map; tuned titles