src/HOL/Library/RBT.thy
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:31 +0200 kuncar new theorem
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Tue, 31 Jul 2012 13:55:39 +0200 kuncar use lifting/transfer formalization of RBT from Lift_RBT
Fri, 13 Apr 2012 11:45:30 +0200 Andreas Lochbihler move RBT implementation into type class contexts
Tue, 21 Feb 2012 12:20:33 +0100 bulwahn subtype preprocessing in Quickcheck;
Fri, 06 Jan 2012 10:19:49 +0100 haftmann incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
Tue, 20 Dec 2011 17:40:18 +0100 bulwahn adding quickcheck generators in some HOL-Library theories
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Wed, 01 Jun 2011 09:10:13 +0200 bulwahn splitting RBT theory into RBT and RBT_Mapping
Thu, 18 Nov 2010 18:53:36 +0100 haftmann proper qualification needed due to shadowing on theory merge
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, 18 Jun 2010 15:26:02 +0200 haftmann prefer fold over foldl
Fri, 21 May 2010 15:22:37 +0200 haftmann tuned
Thu, 20 May 2010 17:29:43 +0200 haftmann implement Mapping.map_entry
Wed, 21 Apr 2010 11:23:04 +0200 hoelzl merged
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;
Thu, 15 Apr 2010 12:27:14 +0200 haftmann theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
Sat, 06 Mar 2010 15:31:30 +0100 haftmann some lemma refinements
Sat, 06 Mar 2010 09:58:28 +0100 haftmann added bulkload; tuned document
Fri, 05 Mar 2010 17:55:14 +0100 haftmann moved lemma map_sorted_distinct_set_unique
Fri, 05 Mar 2010 17:51:29 +0100 haftmann various refinements
Wed, 03 Mar 2010 17:21:45 +0100 haftmann restructured RBT theory
Wed, 03 Mar 2010 08:28:33 +0100 haftmann more explicit naming scheme
Tue, 28 Jul 2009 08:49:03 +0200 krauss tuned
Mon, 27 Jul 2009 22:50:04 +0200 krauss added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
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
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Mon, 03 Mar 2008 14:03:19 +0100 krauss new theory of red-black trees, an efficient implementation of finite maps.
less more (0) tip