| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:42:06 +0200 |
wenzelm |
setsum syntax;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Sat, 10 Feb 2001 08:49:36 +0100 |
ballarin |
Definition of setsum (sort constraint) relaxed to {zero, plus}.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2000 11:41:25 +0200 |
paulson |
now setsum f A = 0 unless A is finite
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:49:05 +0200 |
paulson |
setsum is now overloaded on plus_ac0
|
file |
diff |
annotate
|
| Wed, 27 Oct 1999 19:32:19 +0200 |
oheimb |
added various little lemmas
|
file |
diff |
annotate
|
| Fri, 04 Dec 1998 10:42:53 +0100 |
paulson |
locales: assumes and defines may be empty
|
file |
diff |
annotate
|
| Sat, 31 Oct 1998 12:42:34 +0100 |
paulson |
locales now implicitly quantify over free variables
|
file |
diff |
annotate
|
| Fri, 09 Oct 1998 11:15:07 +0200 |
nipkow |
New inductive definition of `card'
|
file |
diff |
annotate
|
| Tue, 06 Oct 1998 14:39:53 +0200 |
nipkow |
Merges FoldSet into Finite
|
file |
diff |
annotate
|
| Tue, 30 Jun 1998 20:50:34 +0200 |
berghofe |
Adapted to new inductive package.
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 14:39:22 +0200 |
nipkow |
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
|
file |
diff |
annotate
|
| Tue, 03 Jun 1997 10:53:58 +0200 |
paulson |
New theorem about the cardinality of the powerset (uses exponentiation)
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:16:44 +0200 |
paulson |
Now Divides must be the parent
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 14:12:24 +0100 |
clasohm |
added constdefs section
|
file |
diff |
annotate
|
| Mon, 04 Mar 1996 14:37:33 +0100 |
nipkow |
Added a constant UNIV == {x.True}
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:27:16 +0100 |
clasohm |
expanded tabs; renamed subtype to typedef;
|
file |
diff |
annotate
|
| Wed, 29 Nov 1995 16:44:59 +0100 |
clasohm |
removed quotes from types in consts and syntax sections
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|