src/HOL/Data_Structures/RBT_Set.thy
Fri, 27 Dec 2019 10:54:15 +0100 nipkow tuned
Wed, 25 Sep 2019 17:22:57 +0200 nipkow replaced new type ('a,'b) tree by old type ('a*'b) tree.
Mon, 16 Sep 2019 18:00:27 +0200 nipkow tuned
Mon, 19 Aug 2019 16:49:24 +0200 nipkow tuned names
Sun, 16 Sep 2018 15:16:04 +0200 nipkow more traditional formulation
Wed, 13 Jun 2018 15:24:20 +0200 nipkow qualify interpretations to avoid clashes
Tue, 12 Jun 2018 17:18:40 +0200 nipkow more abstract naming
Mon, 11 Jun 2018 16:29:27 +0200 nipkow tuned order of arguments
Sun, 08 Apr 2018 12:31:08 +0200 nipkow moved and renamed lemmas
Sat, 07 Apr 2018 22:09:57 +0200 nipkow tuned
Sat, 02 Dec 2017 16:50:53 +0000 haftmann more simplification rules
Thu, 15 Jun 2017 11:11:36 +0200 nipkow tuned
Wed, 14 Jun 2017 19:39:12 +0200 nipkow simplified delete/proof
Sat, 28 Jan 2017 15:12:19 +0100 nipkow split balance into two, clearer etc
Fri, 27 Jan 2017 17:35:08 +0100 nipkow tuned name
Fri, 27 Jan 2017 17:28:10 +0100 nipkow removed unclear clause; slower but clearer
Fri, 27 Jan 2017 12:32:49 +0100 nipkow removed contribution by Daniel Stuewe, too detailed.
Thu, 26 Jan 2017 17:51:13 +0100 nipkow added concise log height bound lemma
Wed, 25 Jan 2017 18:26:35 +0100 nipkow tuned
Sun, 16 Oct 2016 09:31:05 +0200 haftmann more standardized theorem names for facts involving the div and mod identity
Thu, 07 Jul 2016 18:08:02 +0200 nipkow got rid of class cmp; added height-size proofs by Daniel Stuewe
Sun, 06 Mar 2016 10:33:34 +0100 nipkow tuned
Sun, 29 Nov 2015 19:01:54 +0100 nipkow RBT invariants for insert
Fri, 27 Nov 2015 18:01:13 +0100 nipkow paint root black after insert and delete
Sun, 15 Nov 2015 12:45:28 +0100 nipkow tuned white space
Thu, 05 Nov 2015 18:38:08 +0100 nipkow tuned
Thu, 05 Nov 2015 08:27:14 +0100 nipkow Convertd to 3-way comparisons
Tue, 13 Oct 2015 17:06:37 +0200 nipkow added invar empty
Wed, 23 Sep 2015 09:14:22 +0200 nipkow tuned
Tue, 22 Sep 2015 08:38:25 +0200 nipkow added red black trees
less more (0) tip