Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
Wed, 02 Apr 2008 15:58:29 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Sun, 17 Feb 2008 06:49:53 +0100 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 12:22:05 +0100 |
paulson |
new metis proofs
|
file |
diff |
annotate
|
Mon, 17 Dec 2007 18:27:48 +0100 |
paulson |
tidied some messy proofs
|
file |
diff |
annotate
|
Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Wed, 07 Feb 2007 17:51:38 +0100 |
berghofe |
Adapted to changes in Finite_Set theory.
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Wed, 09 Aug 2006 00:14:28 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 17 May 2006 01:23:41 +0200 |
wenzelm |
prefer 'definition' over low-level defs;
|
file |
diff |
annotate
|
Thu, 08 Dec 2005 12:50:04 +0100 |
wenzelm |
tuned sources and proofs
|
file |
diff |
annotate
|
Mon, 01 Aug 2005 19:20:28 +0200 |
wenzelm |
more zcong_sym;
|
file |
diff |
annotate
|
Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
Fri, 01 Jul 2005 17:41:10 +0200 |
nipkow |
prime is a predicate now.
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
Sun, 12 Dec 2004 16:25:47 +0100 |
nipkow |
REorganized Finite_Set
|
file |
diff |
annotate
|
Thu, 09 Dec 2004 18:30:59 +0100 |
nipkow |
First step in reorganizing Finite_Set
|
file |
diff |
annotate
|
Thu, 15 Jul 2004 15:32:32 +0200 |
paulson |
redefining sumr to be a translation to setsum
|
file |
diff |
annotate
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
Thu, 25 Mar 2004 10:32:21 +0100 |
paulson |
new material from Avigad
|
file |
diff |
annotate
|
Thu, 20 Mar 2003 15:58:25 +0100 |
paulson |
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
|
file |
diff |
annotate
|