src/HOL/Real/RealPow.thy
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.