src/HOL/Real/ROOT.ML
2003-11-21 paulson 2003-11-21 HOL: installation of Ring_and_Field as the basis for Naturals and Reals
2002-01-13 wenzelm 2002-01-13 Real/Complex_Numbers.thy;
2000-12-30 paulson 2000-12-30 tidying, and separation of HOL-Hyperreal from HOL-Real
2000-09-27 wenzelm 2000-09-27 proper Hyperreal setup;
2000-09-21 fleuriot 2000-09-21 Updated Files with new theorems
2000-07-24 wenzelm 2000-07-24 tuned;
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