| Wed, 02 Jan 2002 16:06:31 +0100 |
paulson |
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Tue, 12 Dec 2000 11:58:44 +0100 |
paulson |
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)
|
file |
diff |
annotate
|
| Wed, 15 Nov 2000 19:42:58 +0100 |
wenzelm |
renamed integ_le_less to int_le_less;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 18:47:30 +0200 |
paulson |
more integer theorems, better simplification
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 11:55:47 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
file |
diff |
annotate
|
| Sat, 12 Aug 2000 21:41:42 +0200 |
paulson |
deleted needless rules
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Wed, 03 May 2000 18:33:28 +0200 |
paulson |
Installation of CombineNumerals for the integers
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:48:23 +0200 |
wenzelm |
simprocs now in IntArith;
|
file |
diff |
annotate
|
| Wed, 08 Sep 1999 15:41:30 +0200 |
paulson |
generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 10:34:54 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:29:30 +0200 |
paulson |
new theorem zless_zero_nat
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:34:00 +0200 |
paulson |
more renaming of theorems from _nat to _int (corresponding to a function that
|
file |
diff |
annotate
|
| Wed, 14 Jul 1999 10:40:11 +0200 |
paulson |
new montonicity theorems
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:44:13 +0200 |
paulson |
new monotonicity theorems
|
file |
diff |
annotate
|
| Fri, 09 Jul 1999 10:47:42 +0200 |
paulson |
more monotonicity laws for times
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|
| Thu, 01 Jul 1999 10:35:35 +0200 |
paulson |
many new theorems concerning multiplication and (in)equations
|
file |
diff |
annotate
|
| Mon, 24 May 1999 15:54:58 +0200 |
paulson |
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:25:56 +0200 |
paulson |
new lemmas
|
file |
diff |
annotate
|
| Tue, 29 Sep 1998 15:57:42 +0200 |
paulson |
many renamings and changes. Simproc for cancelling common terms in relations
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:57:01 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|