src/HOL/Hyperreal/HTranscendental.thy
2007-05-24 nipkow 2007-05-24 *** empty log message ***
2007-05-16 huffman 2007-05-16 minimize imports
2007-05-08 huffman 2007-05-08 fix proof of hypreal_sqrt_sum_squares_ge1
2007-04-13 huffman 2007-04-13 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
2007-03-14 huffman 2007-03-14 move sqrt_divide_self_eq to NthRoot.thy
2006-12-14 huffman 2006-12-14 remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq
2006-12-13 huffman 2006-12-13 remove uses of star_n and FreeUltrafilterNat
2006-12-13 huffman 2006-12-13 remove use of FreeUltrafilterNat
2006-12-13 huffman 2006-12-13 generalized some lemmas; removed redundant lemmas; cleaned up some proofs
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-09 wenzelm 2006-10-09 attribute symmetric: zero_var_indexes;
2006-09-27 huffman 2006-09-27 reorganized HNatInfinite proofs; simplified and renamed some lemmas
2006-09-24 huffman 2006-09-24 remove extra dependencies
2006-09-18 huffman 2006-09-18 replace (x + - y) with (x - y)
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-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-09-12 huffman 2005-09-12 added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
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-07 huffman 2005-09-07 replace type hypnat with nat star
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
2005-08-03 avigad 2005-08-03 changes from renaming of exp_ge_add_one_self
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
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-26 paulson 2004-07-26 converting Hyperreal/Transcendental to Isar script
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-04-22 paulson 2004-04-22 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate places
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-01 paulson 2004-03-01 converted Hyperreal/HTranscendental to Isar script
2003-05-05 paulson 2003-05-05 New material on integration, etc. Moving Hyperreal/ex to directory Complex