| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 06 Sep 2004 15:57:58 +0200 |
paulson |
new "respects" syntax for the congruent operator
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 16:21:57 +0200 |
paulson |
updated treatment of znegative and nat_of
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:48:15 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Sat, 07 Sep 2002 22:04:28 +0200 |
paulson |
conversion of ZF/Integ/{Int,Bin} to Isar scripts
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Mon, 21 May 2001 14:52:27 +0200 |
paulson |
the rest of integer division
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 00:18:36 +0200 |
wenzelm |
tuned symbols;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 17:36:37 +0200 |
paulson |
a number of new theorems
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 18:46:02 +0200 |
paulson |
X-symbols for ordinal, cardinal, integer arithmetic
|
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
|
| 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
|
| Fri, 14 Jul 2000 13:39:03 +0200 |
paulson |
changed the quotient syntax from / to //
|
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
|