2007-05-31 huffman 2007-05-31 replace (- 1) with -1
2007-05-22 huffman 2007-05-22 rename lemmas LIM_ident, isCont_ident, DERIV_ident
2007-05-17 huffman 2007-05-17 cleaned up proof of Maclaurin_sin_bound
2007-05-16 huffman 2007-05-16 minimize imports
2006-12-12 huffman 2006-12-12 add type annotation
2006-09-30 huffman 2006-09-30 add type annotations for DERIV
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2005-07-27 paulson 2005-07-27 removed the dependence on abs_mult
2005-07-13 avigad 2005-07-13 Additions to the Real (and Hyperreal) libraries: RealDef.thy: lemmas relating nats, ints, and reals reversed direction of real_of_int_mult, etc. (now they agree with nat versions) SEQ.thy and Series.thy: various additions RComplete.thy: lemmas involving floor and ceiling introduced natfloor and natceiling Log.thy: various additions
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-05-09 paulson 2005-05-09 from simplesubst to new subst
2005-03-02 nipkow 2005-03-02 another reorganization of setsums and intervals
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2005-02-18 nipkow 2005-02-18 starting to get rid of sumr
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-05 paulson 2004-10-05 new simprules for abs and for things like a/b<1
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-28 paulson 2004-07-28 abs notation
2004-07-28 paulson 2004-07-28 conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2001-11-16 paulson 2001-11-16 even more theories from Jacques