src/HOL/Real/PNat.ML
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-07 paulson 2000-06-07 First round of changes, towards installation of simprocs * replacing 0r by (0::real0 * better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.
2000-05-12 paulson 2000-05-12 tidied
2000-05-10 wenzelm 2000-05-10 fixed theory deps;
1999-09-21 wenzelm 1999-09-21 tuned;
1999-08-19 paulson 1999-08-19 real literals using binary arithmetic
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.
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1998-10-23 oheimb 1998-10-23 corrected auto_tac (applications of unsafe wrappers)
1998-10-01 paulson 1998-10-01 Revised version with Abelian group simprocs
1998-09-10 paulson 1998-09-10 well-formed asym rules; misc. tidying
1998-08-06 nipkow 1998-08-06 Removed duplicate thms (see comment to Arith.ML)
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real