src/HOL/Real/RealDef.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.
1999-11-23 paulson 1999-11-23 distributive laws for * over -
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-09-01 wenzelm 1999-09-01 bind_thms;
1999-08-19 paulson 1999-08-19 real literals using binary arithmetic
1999-08-16 paulson 1999-08-16 inserted Id: lines
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-07-23 paulson 1999-07-23 heavily revised by Jacques: coercions have alphabetic names; exponentiation is available, etc.
1998-10-01 paulson 1998-10-01 Revised version with Abelian group simprocs