src/HOL/Map.thy
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2013-09-24 nipkow 2013-09-24 added lemmas
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2012-02-22 bulwahn 2012-02-22 removing some unnecessary premises from Map theory
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-03-30 bulwahn 2011-03-30 renewing specifications in HOL: replacing types by type_synonym
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-10-10 krauss 2010-10-10 removed output syntax "'a ~=> 'b" for "'a => 'b option"
2010-09-13 haftmann 2010-09-13 moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
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-03-06 haftmann 2010-03-06 lemma restrict_complement_singleton_eq
2010-03-06 haftmann 2010-03-06 added dom_option_map, map_of_map_keys
2010-03-04 haftmann 2010-03-04 lemmas set_map_of_compr, map_of_inject_set
2010-03-03 haftmann 2010-03-03 merged
2010-03-03 haftmann 2010-03-03 more uniform naming conventions
2010-03-02 wenzelm 2010-03-02 proper (type_)notation;
2010-02-17 haftmann 2010-02-17 added lemma map_of_map_restrict; generalized lemma dom_const
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-01-31 haftmann 2010-01-31 more correspondence lemmas between related operations
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2009-11-12 haftmann 2009-11-12 moved lemma map_of_zip_map to Map.thy
2009-07-27 krauss 2009-07-27 some lemmas about maps (contributed by Peter Lammich)
2009-06-02 haftmann 2009-06-02 added/moved lemmas by Andreas Lochbihler
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-04-16 haftmann 2009-04-16 dropped unnamed infix
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2009-01-23 haftmann 2009-01-23 lemmas dom_const, dom_if
2008-11-14 haftmann 2008-11-14 lemmas about dom and minus / insert
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-03-27 haftmann 2008-03-27 lemmas about map_of (zip _ _)
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2007-12-17 haftmann 2007-12-17 whitespace typo
2007-11-28 haftmann 2007-11-28 (reverted to unnamed infix)
2007-11-28 haftmann 2007-11-28 dropped legacy unnamed infix
2007-08-19 nipkow 2007-08-19 Made UN_Un simp
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-02-02 nipkow 2007-02-02 a few additions and deletions
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-30 wenzelm 2006-09-30 tuned specifications and proofs;
2006-06-24 wenzelm 2006-06-24 fixed translations for _MapUpd: CONST;
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-04-09 nipkow 2006-04-09 Made "empty" an abbreviation.
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
2005-09-29 paulson 2005-09-29 simprules need names
2005-09-14 wenzelm 2005-09-14 @{term [source] ...} in subsections probably more robust;
2005-09-14 schirmer 2005-09-14 removed syntax fun_map_comp; introduced map_comp;
2005-04-11 nipkow 2005-04-11 tuned
2005-04-11 nipkow 2005-04-11 tuned Map, renamed lex stuff in List.
2005-04-10 nipkow 2005-04-10 _(_|_) is now override_on
2004-12-03 paulson 2004-12-03 tidied