src/HOL/Real/Real.thy
2004-02-03 paulson 2004-02-03 further tidying of the complex numbers
2002-01-13 wenzelm 2002-01-13 HOL-Real/Complex_Numbers;
2000-07-25 wenzelm 2000-07-25 tuned deps;
1999-09-23 paulson 1999-09-23 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or RealAbs. RealAbs proofs have been highly streamlined. A couple of RealPow proofs use #1, #2, etc.
1999-09-21 wenzelm 1999-09-21 tuned;
1999-08-24 wenzelm 1999-08-24 Real/Real.thy main entry point;
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.
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