| Tue, 11 May 2004 20:11:08 +0200 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |
| Mon, 15 Mar 2004 10:46:01 +0100 |
new lemma
|
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 |
| Sun, 29 Feb 2004 23:05:48 +0100 |
Added specific code generator for number_of.
|
file | diff | annotate |
| Tue, 17 Feb 2004 10:41:59 +0100 |
further tweaks to the numeric theories
|
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 |
| Tue, 27 Jan 2004 15:39:51 +0100 |
replacing HOL/Real/PRat, PNat by the rational number development
|
file | diff | annotate |
| Mon, 12 Jan 2004 16:51:45 +0100 |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file | diff | annotate |
| Wed, 10 Dec 2003 15:59:34 +0100 |
Moving some theorems from Real/RealArith0.ML
|
file | diff | annotate |
| Thu, 04 Dec 2003 16:16:36 +0100 |
further simplifications of the integer development; converting more .ML files
|
file | diff | annotate |
| Thu, 04 Dec 2003 10:29:17 +0100 |
Tidying of the integer development; towards removing the
|
file | diff | annotate |
| Mon, 22 Sep 2003 16:04:49 +0200 |
Improved efficiency of code generated for functions int and nat.
|
file | diff | annotate |
| Mon, 12 Aug 2002 17:48:19 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 31 May 2002 07:53:37 +0200 |
Now arith can deal with div/mod arbitrary nat numerals.
|
file | diff | annotate |
| Wed, 15 May 2002 13:50:38 +0200 |
Set up arith to deal with div 2 and mod 2.
|
file | diff | annotate |
| Thu, 07 Mar 2002 23:41:30 +0100 |
renamed nat_number_of to nat_number (avoid clash with separate theorem);
|
file | diff | annotate |
| Mon, 25 Feb 2002 11:27:07 +0100 |
Introduced variants of operators + * ~ constrained to type int
|
file | diff | annotate |
| Wed, 23 Jan 2002 16:58:05 +0100 |
tuned;
|
file | diff | annotate |
| Mon, 10 Dec 2001 15:23:19 +0100 |
Added code generator setup.
|
file | diff | annotate |
| Tue, 07 Aug 2001 16:36:52 +0200 |
Tweaks for 1 -> 1'
|
file | diff | annotate |
| Mon, 06 Aug 2001 13:43:24 +0200 |
turned translation for 1::nat into def.
|
file | diff | annotate |
| Fri, 01 Dec 2000 19:53:29 +0100 |
Linear arithmetic now copes with mixed nat/int formulae.
|
file | diff | annotate |
| Thu, 03 Aug 2000 10:52:30 +0200 |
introduction of integer exponentiation
|
file | diff | annotate |
| Mon, 19 Jul 1999 15:27:34 +0200 |
NatBin: binary arithmetic for the naturals
|
file | diff | annotate |