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