src/HOL/Hyperreal/Lim.thy
2007-04-10 huffman 2007-04-10 new LIM/isCont lemmas for abs, of_real, and power
2007-04-08 huffman 2007-04-08 remove redundant lemmas
2007-03-14 huffman 2007-03-14 move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
2006-12-13 huffman 2006-12-13 generalized some lemmas; removed redundant lemmas; cleaned up some proofs
2006-12-12 huffman 2006-12-12 cleaned up; generalized some proofs
2006-12-10 nipkow 2006-12-10 Modified lattice locale
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-16 huffman 2006-11-16 add lemmas LIM_zero_iff, LIM_norm_zero_iff
2006-11-10 huffman 2006-11-10 added bounded_linear and bounded_bilinear locales
2006-11-09 huffman 2006-11-09 added LIM_norm and related lemmas
2006-11-08 huffman 2006-11-08 LIM_compose -> isCont_LIM_compose; cleaned up and reorganized sections
2006-11-04 huffman 2006-11-04 moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
2006-11-01 huffman 2006-11-01 move DERIV_sumr from Series.thy to Lim.thy
2006-11-01 huffman 2006-11-01 generalize type of lemma isCont_Id
2006-10-01 huffman 2006-10-01 generalize more DERIV proofs
2006-09-30 huffman 2006-09-30 generalize proofs of DERIV_isCont and DERIV_mult
2006-09-30 huffman 2006-09-30 generalized some DERIV proofs
2006-09-30 huffman 2006-09-30 add scaleR lemmas
2006-09-30 huffman 2006-09-30 generalize type of DERIV
2006-09-28 huffman 2006-09-28 more reorganizing sections
2006-09-28 huffman 2006-09-28 reorganize sections
2006-09-28 huffman 2006-09-28 add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
2006-09-28 huffman 2006-09-28 generalize type of is(NS)UCont
2006-09-24 huffman 2006-09-24 generalize types of lim and nslim
2006-09-21 huffman 2006-09-21 removed division_by_zero class requirements from several lemmas
2006-09-20 huffman 2006-09-20 change section to subsection
2006-09-18 huffman 2006-09-18 replace (x + - y) with (x - y)
2006-09-17 huffman 2006-09-17 generalize type of (NS)LIM to work on functions with vector space domain types
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 some proofs
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-02-12 kleing 2006-02-12 * include generalised MVT in HyperReal (contributed by Benjamin Porter) * add non-denumerability of continuum in Real, includes closed intervals on real (contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/)
2005-09-09 huffman 2005-09-09 starfun, starset, and other functions on NS types are now polymorphic; many similar theorems have been generalized and merged; (star_n X) replaces (Abs_star(starrel `` {X})); many proofs have been simplified with the transfer tactic.
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
2005-07-27 paulson 2005-07-27 removed the dependence on abs_mult
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
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-04 paulson 2004-10-04 revised simprules for division
2004-09-10 nipkow 2004-09-10 new forward deduction capability for simplifier
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 removal of more iff-rules from RealDef.thy
2004-07-28 paulson 2004-07-28 fixed precedences
2004-07-28 paulson 2004-07-28 conversion of Hyperreal/MacLaurin_lemmas to Isar script
2004-07-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
2003-02-07 nipkow 2003-02-07 (*f -> ( *f because of new comments
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-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
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