src/HOL/Map.thy
22 months ago bulwahn 2017-09-01 more facts on Map.map_of and List.zip
23 months ago bulwahn 2017-08-27 more facts on Map.ran
2017-06-05 haftmann 2017-06-05 executable domain membership checks
2016-09-11 wenzelm 2016-09-11 tuned proofs;
2016-09-09 nipkow 2016-09-09 added lemmas
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-08-04 wenzelm 2015-08-04 eliminated clone;
2015-08-04 wenzelm 2015-08-04 more symbols; more spaces;
2015-08-04 wenzelm 2015-08-04 more symbols;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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