src/HOL/Map.thy
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.
2002-02-21 wenzelm 2002-02-21 removed theory Option;
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2000-10-03 wenzelm 2000-10-03 removed "symbols" syntax for constant "override";
1999-10-27 oheimb 1999-10-27 added various little lemmas
1998-08-12 oheimb 1998-08-12 defined map_upd by translation via fun_upd changed syntax of map_upd to be consistent with that of fun_upd added chg_map, map_upds
1998-07-24 nipkow 1998-07-24 Map.update -> map_upd, Unpdate.update -> fun_upd Problem: macros get confused about two updates.
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1997-10-24 nipkow 1997-10-24 Added the new theory Map.