src/HOL/Real/RealDef.thy
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Fri, 02 Nov 2001 17:55:24 +0100 paulson Numerals and simprocs for types real and hypreal. The abstract
Mon, 08 Oct 2001 15:23:20 +0200 wenzelm sane numerals (stage 3): provide generic "1" on all number types;
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Tue, 16 Jan 2001 12:20:52 +0100 paulson renamings: real_of_nat, real_of_int -> (overloaded) real
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:48:18 +0100 nipkow ^^ -> ```
Thu, 04 Jan 2001 10:23:01 +0100 paulson more tidying, especially to remove real_of_posnat
Sat, 30 Dec 2000 22:13:18 +0100 paulson tidying, and separation of HOL-Hyperreal from HOL-Real
Tue, 12 Dec 2000 12:01:19 +0100 paulson first stage in tidying up Real and Hyperreal.
Wed, 06 Dec 2000 12:34:12 +0100 bauerg converted rinv to inverse;
Wed, 19 Jul 2000 12:33:19 +0200 paulson changed / to // for quotienting; general tidying
Sun, 16 Jul 2000 20:55:56 +0200 wenzelm use split syntax;
Wed, 07 Jun 2000 12:14:18 +0200 paulson First round of changes, towards installation of simprocs
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;
Mon, 02 Nov 1998 12:36:16 +0100 paulson increased precedence of unary minus from 80 to 100
Thu, 01 Oct 1998 18:18:01 +0200 paulson Revised version with Abelian group simprocs
less more (0) tip