| Fri, 27 Jun 2003 13:15:40 +0200 |
paulson |
Conversion of AllocBase to new-style
|
file |
diff |
annotate
|
| Mon, 02 Jun 2003 11:17:52 +0200 |
paulson |
Further tweaks of ZF/UNITY
|
file |
diff |
annotate
|
| Tue, 27 May 2003 11:39:03 +0200 |
paulson |
updating ZF-UNITY with Sidi's new material
|
file |
diff |
annotate
|
| Thu, 23 Jan 2003 10:30:14 +0100 |
paulson |
tidying (by script)
|
file |
diff |
annotate
|
| Tue, 01 Oct 2002 13:26:10 +0200 |
paulson |
Numerous cosmetic changes, prompted by the new simplifier
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:47:03 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 11:03:05 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 21 Aug 2002 15:55:40 +0200 |
paulson |
new lemmas
|
file |
diff |
annotate
|
| Fri, 19 Jul 2002 13:28:19 +0200 |
paulson |
A couple of new theorems for Constructible
|
file |
diff |
annotate
|
| Thu, 18 Jul 2002 10:37:55 +0200 |
paulson |
new theorems to support Constructible proofs
|
file |
diff |
annotate
|
| Sun, 14 Jul 2002 15:14:43 +0200 |
paulson |
improved presentation markup
|
file |
diff |
annotate
|
| Wed, 10 Jul 2002 16:54:07 +0200 |
paulson |
Fixed quantified variable name preservation for ball and bex (bounded quants)
|
file |
diff |
annotate
|
| Tue, 09 Jul 2002 23:03:21 +0200 |
paulson |
converted List to new-style
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 12:45:52 +0100 |
paulson |
new definitions from Sidi Ehmety
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 10:29:54 +0200 |
paulson |
instantiated Cancel_Numerals for "nat" in ZF
|
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
|
| Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 18:23:31 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Thu, 23 Jan 1997 10:40:21 +0100 |
wenzelm |
turned some consts into syntax;
|
file |
diff |
annotate
|
| Tue, 20 Aug 1996 12:36:58 +0200 |
paulson |
Addition of function set_of_list
|
file |
diff |
annotate
|
| Mon, 17 Jun 1996 16:50:08 +0200 |
paulson |
Converted to use constdefs instead of defs
|
file |
diff |
annotate
|
| Tue, 06 Feb 1996 12:27:17 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Sat, 09 Dec 1995 13:36:11 +0100 |
clasohm |
removed quotes from consts and syntax sections
|
file |
diff |
annotate
|
| Mon, 19 Dec 1994 15:30:30 +0100 |
lcp |
removed quotes around "Datatype",
|
file |
diff |
annotate
|
| Tue, 29 Nov 1994 00:31:31 +0100 |
lcp |
replaced "rules" by "defs"
|
file |
diff |
annotate
|
| Tue, 06 Sep 1994 11:02:16 +0200 |
lcp |
removal of needless quotes
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 12:51:34 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|
| Tue, 16 Nov 1993 14:24:21 +0100 |
clasohm |
made pseudo theories for all ML files;
|
file |
diff |
annotate
|