src/HOL/Library/Mapping.thy
2013-02-15 haftmann 2013-02-15 attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary
2012-10-24 huffman 2012-10-24 transfer package: more flexible handling of equality relations using is_equality predicate
2012-10-22 kuncar 2012-10-22 new theorems
2012-10-19 kuncar 2012-10-19 don't include Quotient_Option - workaround to a transfer bug
2012-10-18 kuncar 2012-10-18 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
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-18 haftmann 2010-11-18 mapper for mapping type
2010-09-13 haftmann 2010-09-13 established emerging canonical names *_eqI and *_eq_iff
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-02 haftmann 2010-07-02 explicit code_datatype declaration prevents multiple instantiations later on
2010-07-02 haftmann 2010-07-02 refrain from using datatype declaration -- opens chance for quickcheck later on
2010-06-02 haftmann 2010-06-02 hide default, map_entry, map_default
2010-05-24 haftmann 2010-05-24 more lemmas
2010-05-21 haftmann 2010-05-21 more lemmas about mappings, in particular keys
2010-05-20 haftmann 2010-05-20 operations default, map_entry, map_default; more lemmas
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 lemma is_empty_empty
2010-02-17 haftmann 2010-02-17 added ordered_keys
2010-02-17 haftmann 2010-02-17 more close integration with theory Map
2009-11-12 hoelzl 2009-11-12 Remove map_compose, replaced by map_map
2009-06-04 haftmann 2009-06-04 added trees implementing mappings
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-07 haftmann 2009-02-07 Isar proof
2009-02-07 haftmann 2009-02-07 added bulkload
2009-02-07 haftmann 2009-02-07 added bulkload
2009-02-06 haftmann 2009-02-06 added replace operation
2009-02-02 haftmann 2009-02-02 added Mapping.thy to Library