src/HOL/Real/RealDef.thy
Mon, 16 Aug 1999 18:41:32 +0200 paulson inserted Id: lines
Thu, 29 Jul 1999 12:44:57 +0200 paulson added parentheses to cope with a possible reduction of the precedence of unary
Fri, 23 Jul 1999 17:29:12 +0200 paulson heavily revised by Jacques: coercions have alphabetic names;
less more (0) -3 tip