src/HOL/Hyperreal/Transcendental.thy
2007-05-20 huffman 2007-05-20 add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
2007-05-20 huffman 2007-05-20 moved sqrt lemmas from Transcendental.thy to NthRoot.thy
2007-05-20 huffman 2007-05-20 remove obsolete DERIV_ln lemmas
2007-05-20 huffman 2007-05-20 add lemmas about inverse functions; cleaned up proof of polar_ex
2007-05-20 huffman 2007-05-20 rearranged sections
2007-05-19 huffman 2007-05-19 use THE instead of SOME
2007-05-18 huffman 2007-05-18 use mult_strict_mono instead of real_mult_less_mono
2007-05-17 huffman 2007-05-17 avoid using redundant lemmas from RealDef.thy
2007-05-15 huffman 2007-05-15 clean up polar_Ex proofs; remove unnecessary lemmas
2007-05-15 huffman 2007-05-15 remove simp attribute from various polar_Ex lemmas
2007-05-14 huffman 2007-05-14 tuned proofs
2007-05-14 huffman 2007-05-14 spelling: rename arcos -> arccos
2007-05-14 huffman 2007-05-14 tuned proofs
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-13 huffman 2007-05-13 define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
2007-05-10 huffman 2007-05-10 fix proofs
2007-04-17 huffman 2007-04-17 lemma isCont_inv_fun is same as isCont_inverse_function
2007-04-17 huffman 2007-04-17 moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
2007-04-13 huffman 2007-04-13 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
2007-04-13 huffman 2007-04-13 moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
2007-04-08 huffman 2007-04-08 remove redundant lemmas
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-04 huffman 2006-11-04 moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
2006-10-13 berghofe 2006-10-13 Adapted to changes in FixedPoint theory.
2006-10-05 huffman 2006-10-05 reorganize and speed up termdiffs proofs
2006-10-03 huffman 2006-10-03 rewrite proofs of powser_insidea and termdiffs_aux
2006-09-24 huffman 2006-09-24 generalized types of sums, summable, and suminf
2006-09-24 huffman 2006-09-24 remove extra dependencies
2006-09-24 huffman 2006-09-24 move root and sqrt stuff from Transcendental to NthRoot
2006-09-22 huffman 2006-09-22 define constants with THE instead of SOME
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-09-12 huffman 2006-09-12 realpow_divide -> power_divide
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-07-30 webertj 2006-07-30 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-01-05 wenzelm 2006-01-05 replaced swap by contrapos_np;
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-08-03 avigad 2005-08-03 renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
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-07-01 berghofe 2005-07-01 Simplified some proofs (thanks to strong_setsum_cong).
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 paulson 2005-02-22 removed redundant lemmas and simprules
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 starting to get rid of sumr
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-07 paulson 2004-12-07 made proofs more robust
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-10-12 paulson 2004-10-12 tweaks concerned with poly bug-fixing
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-10-04 paulson 2004-10-04 revised simprules for division
2004-08-18 nipkow 2004-08-18 import -> imports