| Wed, 10 Jul 2002 16:54:07 +0200 |
paulson |
Fixed quantified variable name preservation for ball and bex (bounded quants)
|
file |
diff |
annotate
|
| Thu, 23 May 2002 17:05:21 +0200 |
paulson |
new definition of "apply" and new simprule "beta_if"
|
file |
diff |
annotate
|
| Sat, 18 May 2002 20:08:17 +0200 |
paulson |
converted Arith, Univ, func to Isar format!
|
file |
diff |
annotate
|
| Wed, 07 Nov 2001 18:12:12 +0100 |
paulson |
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 12:11:00 +0200 |
paulson |
deleted the redundant first argument of adjust(a,b)
|
file |
diff |
annotate
|
| 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
|
| Fri, 08 Dec 2000 00:04:34 +0100 |
wenzelm |
unsymbolize;
|
file |
diff |
annotate
|
| Thu, 14 Sep 2000 11:34:13 +0200 |
paulson |
a bit more of division
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 17:36:37 +0200 |
paulson |
a number of new theorems
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 12:34:13 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
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
|