src/HOL/Map.thy
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 17 Jun 2018 20:31:51 +0200 nipkow added simp rules
Sat, 16 Jun 2018 07:13:17 +0200 nipkow moved lemmas from AFP
Fri, 15 Jun 2018 10:45:12 +0200 nipkow Map.empty now qualified to avoid name clashes
Wed, 07 Mar 2018 19:02:22 +0100 wenzelm more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Fri, 01 Sep 2017 09:45:56 +0200 bulwahn more facts on Map.map_of and List.zip
Sun, 27 Aug 2017 06:56:29 +0200 bulwahn more facts on Map.ran
Mon, 05 Jun 2017 15:59:41 +0200 haftmann executable domain membership checks
Sun, 11 Sep 2016 00:14:44 +0200 wenzelm tuned proofs;
Fri, 09 Sep 2016 13:39:21 +0200 nipkow added lemmas
Wed, 10 Aug 2016 09:33:54 +0200 nipkow "split add" -> "split"
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 31 Aug 2015 21:01:21 +0200 wenzelm prefer symbols;
Thu, 27 Aug 2015 21:19:48 +0200 haftmann standardized some occurences of ancient "split" alias
Tue, 04 Aug 2015 23:11:16 +0200 wenzelm eliminated clone;
Tue, 04 Aug 2015 14:29:45 +0200 wenzelm more symbols;
Tue, 04 Aug 2015 14:06:24 +0200 wenzelm more symbols;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 14 Apr 2015 11:32:01 +0200 Andreas Lochbihler add lemmas
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Tue, 24 Sep 2013 13:35:27 +0200 nipkow added lemmas
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Wed, 22 Feb 2012 12:30:01 +0100 bulwahn removing some unnecessary premises from Map theory
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 30 Mar 2011 11:32:52 +0200 bulwahn renewing specifications in HOL: replacing types by type_synonym
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Fri, 17 Dec 2010 17:43:54 +0100 wenzelm replaced command 'nonterminals' by slightly modernized version 'nonterminal';
Sun, 10 Oct 2010 22:50:25 +0200 krauss removed output syntax "'a ~=> 'b" for "'a => 'b option"
Mon, 13 Sep 2010 16:43:23 +0200 haftmann moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Sat, 06 Mar 2010 15:31:31 +0100 haftmann lemma restrict_complement_singleton_eq
Sat, 06 Mar 2010 09:58:30 +0100 haftmann added dom_option_map, map_of_map_keys
Thu, 04 Mar 2010 11:22:06 +0100 haftmann lemmas set_map_of_compr, map_of_inject_set
Wed, 03 Mar 2010 20:45:48 +0100 haftmann merged
Wed, 03 Mar 2010 20:45:31 +0100 haftmann more uniform naming conventions
Tue, 02 Mar 2010 23:59:54 +0100 wenzelm proper (type_)notation;
Wed, 17 Feb 2010 09:48:53 +0100 haftmann added lemma map_of_map_restrict; generalized lemma dom_const
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Sun, 31 Jan 2010 14:51:32 +0100 haftmann more correspondence lemmas between related operations
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Thu, 12 Nov 2009 15:10:24 +0100 haftmann moved lemma map_of_zip_map to Map.thy
Mon, 27 Jul 2009 22:50:01 +0200 krauss some lemmas about maps (contributed by Peter Lammich)
Tue, 02 Jun 2009 16:23:43 +0200 haftmann added/moved lemmas by Andreas Lochbihler
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Thu, 16 Apr 2009 14:02:12 +0200 haftmann dropped unnamed infix
Fri, 27 Mar 2009 10:05:11 +0100 haftmann normalized imports
Wed, 04 Mar 2009 10:47:20 +0100 nipkow Made Option a separate theory and renamed option_map to Option.map
Fri, 23 Jan 2009 19:51:48 +0100 haftmann lemmas dom_const, dom_if
Fri, 14 Nov 2008 08:50:08 +0100 haftmann lemmas about dom and minus / insert
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Thu, 27 Mar 2008 19:04:37 +0100 haftmann lemmas about map_of (zip _ _)
less more (0) -100 -60 tip