src/HOL/Library/Dlist.thy
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-18 haftmann 2010-11-18 mapper for dlist type
2010-10-25 haftmann 2010-10-25 dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-04 haftmann 2010-10-04 turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-09-27 haftmann 2010-09-27 lemma remdups_list_of_dlist
2010-09-13 haftmann 2010-09-13 established emerging canonical names *_eqI and *_eq_iff
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-18 haftmann 2010-08-18 added equality instantiation
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy
2010-06-21 haftmann 2010-06-21 extensionality rule fset_eqI
2010-05-24 haftmann 2010-05-24 induction and case rules
2010-05-20 haftmann 2010-05-20 proper code generator for complement
2010-05-20 haftmann 2010-05-20 moved generic List operations to theory More_List
2010-05-19 haftmann 2010-05-19 added implementations of Fset.Set, Fset.Coset; do not delete code equations for relational operators on fsets
2010-04-22 haftmann 2010-04-22 lemma dlist_ext
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-11 haftmann 2010-04-11 user interface for abstract datatypes is an attribute, not a command
2010-03-10 haftmann 2010-03-10 avoid confusion
2010-02-22 haftmann 2010-02-22 added Dlist