src/HOL/Library/Mapping.thy
20 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2017-07-02 haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
2016-07-13 wenzelm 2016-07-13 tuned;
2016-07-12 wenzelm 2016-07-12 misc tuning and modernization;
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-06-06 haftmann 2016-06-06 explicit tagging of code equations de-baroquifies interface
2016-06-01 eberlm 2016-06-01 Tuned code equations for mappings and PMFs
2016-05-31 eberlm 2016-05-31 Added code generation for PMFs
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-31 wenzelm 2015-08-31 proper qualified naming;
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-02-06 haftmann 2015-02-06 non-intrusive default code setup for mappings
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-04-09 haftmann 2014-04-09 restoring notion of primitive vs. derived operations in terms of generated code; established _paramatric suffix for parametricity rules
2014-04-09 haftmann 2014-04-09 removed duplication and tuned
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 blanchet 2014-03-06 renamed 'prod_rel' to 'rel_prod'
2014-03-06 blanchet 2014-03-06 renamed 'set_rel' to 'rel_set'
2014-02-16 blanchet 2014-02-16 folded 'rel_option' into 'option_rel'
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2013-12-23 haftmann 2013-12-23 prefer Y_of_X over X_to_Y; prefer alist over assoc_list; prefer explicit prefix
2013-08-13 traytel 2013-08-13 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
2013-08-13 kuncar 2013-08-13 remove unnecessary dependencies on Library/Quotient_*
2013-03-08 kuncar 2013-03-08 convert mappings to parametric lifting
2013-03-08 kuncar 2013-03-08 patch Isabelle ditribution to conform to changes regarding the parametricity
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