src/HOL/Real/RealDef.thy
Thu, 01 Oct 1998 18:18:01 +0200 Revised version with Abelian group simprocs