| Thu, 29 Jul 1999 12:44:57 +0200 |
paulson |
added parentheses to cope with a possible reduction of the precedence of unary
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:34:37 +0200 |
paulson |
more renaming of theorems from _nat to _int (corresponding to a function that
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:44:45 +0200 |
paulson |
renamed inj_nat to inj_int
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|
| Wed, 23 Jun 1999 10:37:29 +0200 |
paulson |
new distributive laws involving * and -
|
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
|
| Fri, 21 May 1999 10:47:07 +0200 |
paulson |
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 12:16:34 +0100 |
nipkow |
Refined arithmetic.
|
file |
diff |
annotate
|
| Mon, 11 Jan 1999 16:50:49 +0100 |
nipkow |
More arith simplifications.
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 20:44:34 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:27:17 +0200 |
paulson |
much tidying
|
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
|
| Wed, 23 Sep 1998 10:25:37 +0200 |
paulson |
much renaming and reorganization
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 16:04:00 +0200 |
paulson |
new files in Integ
|
file |
diff |
annotate
|