src/HOL/Library/Mapping.thy
Thu, 19 Aug 2021 12:31:06 +0200 Lukas Stevens add/rename some theorems about Map(pings)
Tue, 01 Jun 2021 19:46:34 +0200 nipkow More general fold function for maps
Wed, 22 Aug 2018 12:32:58 +0000 haftmann removed ineffective code equation
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 02 Jul 2017 20:13:38 +0200 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
Wed, 13 Jul 2016 19:02:23 +0200 wenzelm tuned;
Tue, 12 Jul 2016 15:45:32 +0200 wenzelm misc tuning and modernization;
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
Mon, 06 Jun 2016 21:28:46 +0200 haftmann explicit tagging of code equations de-baroquifies interface
Wed, 01 Jun 2016 13:48:34 +0200 eberlm Tuned code equations for mappings and PMFs
Tue, 31 May 2016 13:02:44 +0200 eberlm Added code generation for PMFs
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Mon, 31 Aug 2015 20:56:24 +0200 wenzelm proper qualified naming;
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Fri, 06 Feb 2015 08:47:48 +0100 haftmann non-intrusive default code setup for mappings
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
Wed, 09 Apr 2014 14:08:25 +0200 haftmann restoring notion of primitive vs. derived operations in terms of generated code;
Wed, 09 Apr 2014 14:08:18 +0200 haftmann removed duplication and tuned
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:29:18 +0100 blanchet renamed 'prod_rel' to 'rel_prod'
Thu, 06 Mar 2014 14:57:14 +0100 blanchet renamed 'set_rel' to 'rel_set'
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'rel_option' into 'option_rel'
Fri, 14 Feb 2014 07:53:46 +0100 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Mon, 23 Dec 2013 16:29:43 +0100 haftmann prefer Y_of_X over X_to_Y;
Tue, 13 Aug 2013 18:22:55 +0200 traytel got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
Tue, 13 Aug 2013 15:59:22 +0200 kuncar remove unnecessary dependencies on Library/Quotient_*
Fri, 08 Mar 2013 13:21:58 +0100 kuncar convert mappings to parametric lifting
Fri, 08 Mar 2013 13:21:06 +0100 kuncar patch Isabelle ditribution to conform to changes regarding the parametricity
Fri, 15 Feb 2013 11:47:34 +0100 haftmann attempt to re-establish conventions which theories are loaded into the grand unified library theory;
Wed, 24 Oct 2012 18:43:25 +0200 huffman transfer package: more flexible handling of equality relations using is_equality predicate
Mon, 22 Oct 2012 22:47:14 +0200 kuncar new theorems
Fri, 19 Oct 2012 17:54:16 +0200 kuncar don't include Quotient_Option - workaround to a transfer bug
Thu, 18 Oct 2012 15:52:33 +0200 kuncar update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Fri, 21 Oct 2011 11:17:14 +0200 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mapping type
Mon, 13 Sep 2010 16:43:23 +0200 haftmann established emerging canonical names *_eqI and *_eq_iff
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
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Fri, 02 Jul 2010 17:27:44 +0200 haftmann explicit code_datatype declaration prevents multiple instantiations later on
Fri, 02 Jul 2010 16:50:53 +0200 haftmann refrain from using datatype declaration -- opens chance for quickcheck later on
Wed, 02 Jun 2010 22:06:14 +0200 haftmann hide default, map_entry, map_default
Mon, 24 May 2010 13:48:57 +0200 haftmann more lemmas
Fri, 21 May 2010 15:22:37 +0200 haftmann more lemmas about mappings, in particular keys
Thu, 20 May 2010 17:29:43 +0200 haftmann operations default, map_entry, map_default; more lemmas
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Sun, 11 Apr 2010 16:51:06 +0200 haftmann lemma is_empty_empty
Wed, 17 Feb 2010 16:49:37 +0100 haftmann added ordered_keys
Wed, 17 Feb 2010 09:48:52 +0100 haftmann more close integration with theory Map
Thu, 12 Nov 2009 17:21:51 +0100 hoelzl Remove map_compose, replaced by map_map
Thu, 04 Jun 2009 16:55:20 +0200 haftmann added trees implementing mappings
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
less more (0) -60 tip