src/HOL/Hyperreal/Lim.thy
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-02 haftmann 2008-07-02 cleaned up some code generator configuration
2007-06-20 huffman 2007-06-20 avoid using implicit prems in assumption
2007-05-30 huffman 2007-05-30 simplify names of locale interpretations
2007-05-29 huffman 2007-05-29 add isUCont lemmas
2007-05-22 huffman 2007-05-22 generalize uniqueness of limits to class real_normed_algebra_1
2007-05-22 huffman 2007-05-22 rename lemmas LIM_ident, isCont_ident, DERIV_ident
2007-05-20 huffman 2007-05-20 add lemmas LIM_compose2, isCont_LIM_compose2
2007-05-19 huffman 2007-05-19 remove dependence on Hilbert_Choice.thy
2007-04-12 huffman 2007-04-12 moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
2007-04-12 huffman 2007-04-12 new standard proof of lemma LIM_inverse
2007-04-11 huffman 2007-04-11 moved nonstandard stuff from SEQ.thy into new file HSEQ.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