Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 11:04:42 +0200 |
haftmann |
unified curried gcd, lcm, zgcd, zlcm
|
file |
diff |
annotate
|
Mon, 17 Dec 2007 18:27:48 +0100 |
paulson |
tidied some messy proofs
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 11:06:04 +0200 |
chaieb |
tuned Proof
|
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, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
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
|
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
|
Thu, 09 Dec 2004 18:30:59 +0100 |
nipkow |
First step in reorganizing Finite_Set
|
file |
diff |
annotate
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
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
|