| 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 |
| Fri, 23 Apr 2004 11:04:07 +0200 |
congruent2 now allows different equiv relations
|
file | diff | annotate |
| Tue, 30 Mar 2004 11:25:14 +0200 |
tidied
|
file | diff | annotate |
| Thu, 25 Mar 2004 10:31:25 +0100 |
new treatment of equivalence classes
|
file | diff | annotate |
| Fri, 19 Mar 2004 10:50:06 +0100 |
removed redundant thms
|
file | diff | annotate |
| Mon, 08 Mar 2004 11:12:06 +0100 |
generic theorems about exponentials; general tidying up
|
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 |
| Tue, 02 Mar 2004 11:06:37 +0100 |
fixed bugs in the setup of arithmetic procedures
|
file | diff | annotate |
| Mon, 01 Mar 2004 13:51:21 +0100 |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file | diff | annotate |
| Thu, 19 Feb 2004 15:57:34 +0100 |
Efficient, graph-based reasoner for linear and partial orders.
|
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 |
| 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 |
| Fri, 09 Jan 2004 10:46:18 +0100 |
Defining the type class "ringpower" and deleting superseded theorems for
|
file | diff | annotate |
| Tue, 06 Jan 2004 10:40:15 +0100 |
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
|
file | diff | annotate |
| Thu, 01 Jan 2004 21:47:07 +0100 |
conversion of Real/PReal to Isar script;
|
file | diff | annotate |
| Thu, 01 Jan 2004 10:06:32 +0100 |
tweaking of lemmas in RealDef, RealOrd
|
file | diff | annotate |
| Thu, 25 Dec 2003 22:48:32 +0100 |
re-organized some hyperreal and real lemmas
|
file | diff | annotate |
| Tue, 02 Dec 2003 11:48:15 +0100 |
More re-organising of numerical theorems
|
file | diff | annotate |
| Fri, 28 Nov 2003 12:09:37 +0100 |
conversion of some Real theories to Isar scripts
|
file | diff | annotate |
| Thu, 08 Aug 2002 23:52:55 +0200 |
tuned;
|
file | diff | annotate |
| Fri, 09 Nov 2001 00:09:47 +0100 |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
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, 08 Oct 2001 15:23:20 +0200 |
sane numerals (stage 3): provide generic "1" on all number types;
|
file | diff | annotate |
| Fri, 05 Oct 2001 21:52:39 +0200 |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file | diff | annotate |
| Tue, 16 Jan 2001 12:20:52 +0100 |
renamings: real_of_nat, real_of_int -> (overloaded) real
|
file | diff | annotate |
| Tue, 09 Jan 2001 15:32:27 +0100 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 05 Jan 2001 18:48:18 +0100 |
^^ -> ```
|
file | diff | annotate |
| Thu, 04 Jan 2001 10:23:01 +0100 |
more tidying, especially to remove real_of_posnat
|
file | diff | annotate |
| Sat, 30 Dec 2000 22:13:18 +0100 |
tidying, and separation of HOL-Hyperreal from HOL-Real
|
file | diff | annotate |
| Tue, 12 Dec 2000 12:01:19 +0100 |
first stage in tidying up Real and Hyperreal.
|
file | diff | annotate |
| Wed, 06 Dec 2000 12:34:12 +0100 |
converted rinv to inverse;
|
file | diff | annotate |
| Wed, 19 Jul 2000 12:33:19 +0200 |
changed / to // for quotienting; general tidying
|
file | diff | annotate |
| Sun, 16 Jul 2000 20:55:56 +0200 |
use split syntax;
|
file | diff | annotate |
| Wed, 07 Jun 2000 12:14:18 +0200 |
First round of changes, towards installation of simprocs
|
file | diff | annotate |
| Mon, 16 Aug 1999 18:41:32 +0200 |
inserted Id: lines
|
file | diff | annotate |
| Thu, 29 Jul 1999 12:44:57 +0200 |
added parentheses to cope with a possible reduction of the precedence of unary
|
file | diff | annotate |
| Fri, 23 Jul 1999 17:29:12 +0200 |
heavily revised by Jacques: coercions have alphabetic names;
|
file | diff | annotate |
| Mon, 02 Nov 1998 12:36:16 +0100 |
increased precedence of unary minus from 80 to 100
|
file | diff | annotate |
| Thu, 01 Oct 1998 18:18:01 +0200 |
Revised version with Abelian group simprocs
|
file | diff | annotate |