src/HOL/Library/DAList.thy
2012-03-28 bulwahn 2012-03-28 removing now redundant impl_of theorems in DAList
2012-03-27 bulwahn 2012-03-27 association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements
2012-02-16 wenzelm 2012-02-16 tuned proofs;
2012-01-17 bulwahn 2012-01-17 renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
2012-01-17 bulwahn 2012-01-17 renamed theory AList to DAList