src/HOL/NthRoot.thy
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-01-11 paulson 2016-01-11 nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-30 paulson 2015-06-30 Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-06-02 hoelzl 2014-06-02 remove superfluous assumption
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-07 paulson 2014-03-07 a few new lemmas
2013-11-12 hoelzl 2013-11-12 add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
2013-09-12 huffman 2013-09-12 prefer attribute 'unfolded thm' to 'simplified'
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-03-22 hoelzl 2013-03-22 modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-10 wenzelm 2012-10-10 eliminated spurious fact duplicates;
2011-08-20 huffman 2011-08-20 remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-19 huffman 2011-08-19 remove some redundant simp rules about sqrt
2011-08-18 huffman 2011-08-18 optimize some proofs
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2009-06-30 hoelzl 2009-06-30 Added DERIV_intros
2009-04-28 haftmann 2009-04-28 collected square lemmas in Nat_Numeral
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s