src/HOL/NthRoot.thy
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