src/HOL/Hyperreal/NthRoot.thy
2007-05-14 huffman 2007-05-14 tuned
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-13 huffman 2007-05-13 removed redundant lemmas
2007-05-08 huffman 2007-05-08 add lemma real_sqrt_sum_squares_triangle_ineq
2007-05-08 huffman 2007-05-08 cleaned up
2007-04-17 huffman 2007-04-17 moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
2007-04-11 huffman 2007-04-11 move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
2007-03-14 huffman 2007-03-14 move sqrt_divide_self_eq to NthRoot.thy
2006-12-16 huffman 2006-12-16 moved several theorems; rearranged theory dependencies
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-24 huffman 2006-09-24 move root and sqrt stuff from Transcendental to NthRoot
2006-09-12 huffman 2006-09-12 remove extra dependency
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-01-05 wenzelm 2006-01-05 replaced swap by contrapos_np;
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
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-05-21 wenzelm 2004-05-21 tuned document;
2004-03-19 paulson 2004-03-19 conversion of Hyperreal/Lim to new-style
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2004-01-14 nipkow 2004-01-14 Told linear arithmetic package about injections "real" from nat/int into real.
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-23 paulson 2003-12-23 removing real_of_posnat
2003-12-23 paulson 2003-12-23 converting Hyperreal/NthRoot to Isar
2003-11-27 paulson 2003-11-27 Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files. New theorems for Ring_and_Field. Fixing affected proofs.
2001-11-15 paulson 2001-11-15 new theories from Jacques Fleuriot