src/HOL/Library/FrechetDeriv.thy
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-09 huffman 2011-08-09 lemma bounded_linear_intro
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-04 huffman 2010-07-04 uniqueness of Frechet derivative
2010-04-30 huffman 2010-04-30 remove duplicate lemmas
2010-04-25 huffman 2010-04-25 fix duplicate simp rule warnings
2009-12-18 huffman 2009-12-18 rename equals_zero_I to minus_unique (keep old name too)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-18 huffman 2009-02-18 move FrechetDeriv.thy to Library