src/HOL/Map.thy
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
2004-11-21 nipkow 2004-11-21 Added more lemmas
2004-11-21 nipkow 2004-11-21 added lemmas
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-04 nipkow 2004-08-04 Added a number of new thms and the new function remove1
2004-05-12 nipkow 2004-05-12 renamed `> to o_m
2004-04-12 oheimb 2004-04-12 added theorem chg_map_other
2004-02-05 nipkow 2004-02-05 Changed variable names.
2003-12-18 nipkow 2003-12-18 *** empty log message ***
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-14 nipkow 2003-09-14 Added new theorems
2003-09-11 nipkow 2003-09-11 Added a number of thms about map restriction.
2003-09-03 nipkow 2003-09-03 Introduced new syntax for maplets x |-> y
2003-07-25 nipkow 2003-07-25 Replaced \<leadsto> by \<rightharpoonup>
2003-07-11 oheimb 2003-07-11 added map_image, restrict_map, some thms
2003-05-16 webertj 2003-05-16 Added a few lemmas about map_le
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2003-04-30 nipkow 2003-04-30 added a thm
2003-04-16 nipkow 2003-04-16 header
2003-04-15 kleing 2003-04-15 fixed document
2003-04-14 nipkow 2003-04-14 Added thms
2003-04-14 webertj 2003-04-14 Fixed non-escaped underscore in section headings (document generation should work again now).
2003-04-11 webertj 2003-04-11 Map.ML integrated into Map.thy
2003-04-01 nipkow 2003-04-01 Made empty a translation rather than a constant.