src/HOL/Library/DAList.thy
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-08-12 traytel 2015-08-12 use lift_bnf in an example
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-03-04 traytel 2015-03-04 alist is a BNF
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-28 wenzelm 2014-10-28 tuned proofs; tuned white space; more symbols;
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
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