src/HOL/Real/ROOT.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-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-30 wenzelm 2000-05-30 cleaned up;
2000-05-10 wenzelm 2000-05-10 fixed theory deps;
1999-10-27 paulson 1999-10-27 TEMPORARY use of Addsimps
1999-10-26 wenzelm 1999-10-26 do not set proof_timing;
1999-09-23 nipkow 1999-09-23 Restructured lin.arith.package and fixed a proof in RComplete.
1999-08-24 wenzelm 1999-08-24 Real/Real.thy main entry point;
1999-08-19 paulson 1999-08-19 real literals using binary arithmetic
1999-08-16 paulson 1999-08-16 inserted Id: lines
1999-04-22 wenzelm 1999-04-22 improved load paths;
1999-03-11 wenzelm 1999-03-11 removed foo_build_completed -- now handled by session management (via usedir);
1999-02-05 wenzelm 1999-02-05 add_path;
1998-11-27 paulson 1998-11-27 Addition of Hyperreal theories Zorn and Filter
1998-10-01 paulson 1998-10-01 Revised version with Abelian group simprocs
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real