src/HOL/Library/DAList.thy
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