| Tue, 11 May 2004 20:11:08 +0200 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |
| Sat, 01 May 2004 22:01:57 +0200 |
tuned instance statements;
|
file | diff | annotate |
| Tue, 13 Apr 2004 07:48:32 +0200 |
hence -> from calculation have
|
file | diff | annotate |
| Thu, 04 Mar 2004 12:06:07 +0100 |
new material from Avigad, and simplified treatment of division by 0
|
file | diff | annotate |
| Sun, 15 Feb 2004 10:46:37 +0100 |
Polymorphic treatment of binary arithmetic using axclasses
|
file | diff | annotate |
| Tue, 10 Feb 2004 12:02:11 +0100 |
generic of_nat and of_int functions, and generalization of iszero
|
file | diff | annotate |
| Thu, 05 Feb 2004 10:45:28 +0100 |
tidying up, especially the Complex numbers
|
file | diff | annotate |
| Wed, 28 Jan 2004 17:01:01 +0100 |
tidying up arithmetic for the hyperreals
|
file | diff | annotate |
| Tue, 27 Jan 2004 15:39:51 +0100 |
replacing HOL/Real/PRat, PNat by the rational number development
|
file | diff | annotate |
| Thu, 01 Jan 2004 21:47:07 +0100 |
conversion of Real/PReal to Isar script;
|
file | diff | annotate |
| Fri, 02 Nov 2001 17:55:24 +0100 |
Numerals and simprocs for types real and hypreal. The abstract
|
file | diff | annotate |
| Mon, 11 Oct 1999 10:52:51 +0200 |
replaced {x. True} by UNIV to work with the new simprule, Collect_const
|
file | diff | annotate |
| Mon, 16 Aug 1999 18:41:32 +0200 |
inserted Id: lines
|
file | diff | annotate |
| Fri, 23 Jul 1999 17:29:12 +0200 |
heavily revised by Jacques: coercions have alphabetic names;
|
file | diff | annotate |
| Thu, 25 Jun 1998 13:57:34 +0200 |
Installation of target HOL-Real
|
file | diff | annotate |