src/HOL/Hyperreal/Series.thy
2006-09-16 huffman 2006-09-16 generalized types of many constants to work over arbitrary vector spaces; modified theorems using Rep_star to eliminate existential quantifiers
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-08-23 huffman 2006-08-23 speed up proof of summable_Cauchy
2006-07-29 webertj 2006-07-29 lin_arith_prover splits certain operators (e.g. min, max, abs)
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;
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2006-02-19 kleing 2006-02-19 * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) * added Complex/ex/ASeries_Complex (instantiation of the above for reals) * added Complex/ex/HarmonicSeries (should really be in something like Complex/Library) (these are contributions by Benjamin Porter, numbers 68 and 34 of http://www.cs.ru.nl/~freek/100/)
2005-08-26 ballarin 2005-08-26 Lemmas on dvd, power and finite summation added or strengthened.
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-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-03-02 nipkow 2005-03-02 another reorganization of setsums and intervals
2005-02-23 nipkow 2005-02-23 suminf -> \<Sum>
2005-02-22 nipkow 2005-02-22 more setsum tuning
2005-02-21 nipkow 2005-02-21 more fine tuniung
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2005-02-18 nipkow 2005-02-18 continued eliminating sumr
2005-02-18 nipkow 2005-02-18 starting to get rid of sumr
2004-12-02 nipkow 2004-12-02 Added "ALL x > y" and relatives.
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-29 paulson 2004-07-29 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-07-16 nipkow 2004-07-16 Corrected TeX problems.
2004-07-15 paulson 2004-07-15 redefining sumr to be a translation to setsum
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-02-26 paulson 2004-02-26 converted Hyperreal/Series to Isar script
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-12-30 paulson 2000-12-30 separation of HOL-Hyperreal from HOL-Real