| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 13:37:10 +0200 |
chaieb |
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 16:13:42 +0200 |
chaieb |
Fixed proofs.
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 11:04:42 +0200 |
haftmann |
unified curried gcd, lcm, zgcd, zlcm
|
file |
diff |
annotate
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Mon, 28 Apr 2008 20:21:11 +0200 |
haftmann |
thms Max_ge, Min_le: dropped superfluous premise
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 14:39:54 +0100 |
chaieb |
Removed theorems from default simpset
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 16:10:54 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 11:59:57 +0100 |
chaieb |
More primality theorems
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:08 +0100 |
haftmann |
explicit import of theory ATP_Linkup
|
file |
diff |
annotate
|
| Wed, 18 Jul 2007 11:43:06 +0200 |
paulson |
tidying using metis
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 21:26:35 +0200 |
wenzelm |
tuned document (headers, sections, spacing);
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 11:39:08 +0200 |
nipkow |
moved gcd to new GCD.thy
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 17:41:10 +0200 |
nipkow |
prime is a predicate now.
|
file |
diff |
annotate
|
| Fri, 25 Mar 2005 16:20:57 +0100 |
paulson |
tidied up
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Thu, 30 May 2002 10:12:52 +0200 |
nipkow |
Modifications due to enhanced linear arithmetic.
|
file |
diff |
annotate
|
| Wed, 06 Mar 2002 17:54:43 +0100 |
wenzelm |
added two_is_prime;
|
file |
diff |
annotate
|
| Sun, 13 Jan 2002 21:14:14 +0100 |
wenzelm |
prime_dvd_power_two;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2001 23:23:33 +0100 |
wenzelm |
gcd_dvd1 and gcd_dvd2 proven simultaneously;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Wed, 13 Jun 2001 16:29:51 +0200 |
paulson |
New proof of gcd_zero after a change to Divides.ML made the old one fail
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 14:22:08 +0200 |
wenzelm |
tuned
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 14:18:19 +0200 |
wenzelm |
tuned Primes theory;
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 08:41:25 +0200 |
paulson |
moved Primes.thy from NumberTheory to Library
|
file |
diff |
annotate
|