| Tue, 26 Jun 2001 17:04:09 +0200 |
paulson |
tidying and consolidating files
|
file |
diff |
annotate
|
| Mon, 21 May 2001 14:52:27 +0200 |
paulson |
the rest of integer division
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:21:07 +0200 |
wenzelm |
tuned ML code (the_context, bind_thms(s));
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 17:36:37 +0200 |
paulson |
a number of new theorems
|
file |
diff |
annotate
|
| Fri, 11 Aug 2000 13:27:17 +0200 |
paulson |
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
|
file |
diff |
annotate
|
| Fri, 11 Aug 2000 10:34:02 +0200 |
paulson |
interim working version: more improvements to the integers
|
file |
diff |
annotate
|
| Thu, 10 Aug 2000 11:27:34 +0200 |
paulson |
installation of cancellation simprocs for the integers
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 10:29:54 +0200 |
paulson |
instantiated Cancel_Numerals for "nat" in ZF
|
file |
diff |
annotate
|
| Wed, 02 Aug 2000 16:07:32 +0200 |
paulson |
coercion "intify" to remove type constraints from integer algebraic laws
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 15:28:21 +0200 |
paulson |
natify, a coercion to reduce the number of type constraints in arithmetic
|
file |
diff |
annotate
|
| Fri, 14 Jul 2000 13:39:03 +0200 |
paulson |
changed the quotient syntax from / to //
|
file |
diff |
annotate
|
| Mon, 07 Feb 2000 15:14:02 +0100 |
paulson |
tidied some proofs
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 10:31:31 +0100 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 20:44:34 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:18:07 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|