src/HOL/Real/RealPow.thy
2007-05-24 nipkow 2007-05-24 *** empty log message ***
2007-05-14 huffman 2007-05-14 move lemmas to RealPow.thy; tuned proofs
2007-05-14 huffman 2007-05-14 added general sum-squares lemmas
2007-05-14 huffman 2007-05-14 remove redundant lemmas
2007-05-14 huffman 2007-05-14 cleaned up
2007-05-13 nipkow 2007-05-13 Removed junk
2007-04-10 huffman 2007-04-10 removed unnecessary premise from power_le_imp_le_base
2006-09-20 huffman 2006-09-20 add header
2006-09-12 huffman 2006-09-12 simplify some proofs, remove obsolete realpow_divide
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
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-29 paulson 2004-07-29 removed some [iff] declarations from RealDef.thy, concerning inequalities
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-02-18 paulson 2004-02-18 removed obsolete theorem
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-01-12 paulson 2004-01-12 Modified real arithmetic simplification
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-19 paulson 2003-12-19 minor tweaks
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
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.
2003-11-21 paulson 2003-11-21 HOL: installation of Ring_and_Field as the basis for Naturals and Reals
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-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-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-07-25 wenzelm 2000-07-25 lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
2000-06-01 fleuriot 2000-06-01 Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.
2000-05-10 wenzelm 2000-05-10 fixed theory deps;
1999-08-16 paulson 1999-08-16 inserted Id: lines
1999-07-23 paulson 1999-07-23 heavily revised by Jacques: coercions have alphabetic names; exponentiation is available, etc.