src/HOL/Library/FrechetDeriv.thy
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Tue, 09 Aug 2011 12:50:22 -0700 huffman lemma bounded_linear_intro
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
Sun, 04 Jul 2010 09:25:17 -0700 huffman uniqueness of Frechet derivative
Fri, 30 Apr 2010 13:51:17 -0700 huffman remove duplicate lemmas
Sun, 25 Apr 2010 23:22:29 -0700 huffman fix duplicate simp rule warnings
Fri, 18 Dec 2009 19:00:11 -0800 huffman rename equals_zero_I to minus_unique (keep old name too)
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 18 Feb 2009 19:51:39 -0800 huffman move FrechetDeriv.thy to Library
less more (0) tip