src/HOL/Data_Structures/AVL_Set.thy
Fri, 07 Aug 2020 11:46:14 +0200 wenzelm avoid failure of "isabelle build -o skip_proofs";
Wed, 06 May 2020 10:46:19 +0200 nipkow tuned
Tue, 05 May 2020 20:32:57 +0200 nipkow tuned proofs
Tue, 28 Apr 2020 18:34:59 +0200 nipkow use abs(h l - h r) instead of 3 cases, tuned proofs
Sat, 25 Apr 2020 16:31:43 +0200 nipkow added Height_Balanced_Trees
Thu, 23 Apr 2020 22:54:23 +0200 nipkow split AVL_Set.thy
Tue, 07 Apr 2020 17:03:44 +0200 nipkow more automation and clarification
Wed, 01 Apr 2020 21:48:39 +0200 nipkow simplified code and proofs
Wed, 01 Apr 2020 18:05:02 +0200 nipkow automated proof
Thu, 27 Feb 2020 12:18:16 +0100 nipkow removed dead lemma
Wed, 26 Feb 2020 23:49:16 +0100 nipkow simplified proofs
Mon, 24 Feb 2020 21:43:28 +0100 nipkow tuned var names (avoid h)
less more (0) -12 tip