| Thu, 07 Sep 2000 21:10:11 +0200 |
wenzelm |
updated attribute names;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 13:12:00 +0200 |
paulson |
tidied, proving gcd_greatest_iff and using induct_tac
|
file |
diff |
annotate
|
| Mon, 04 Sep 2000 10:24:55 +0200 |
paulson |
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 10:30:28 +0200 |
nipkow |
made mod_less_divisor a simplification rule.
|
file |
diff |
annotate
|
| Tue, 20 Apr 1999 14:36:19 +0200 |
paulson |
Main is the correct parent
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Fri, 04 Jul 1997 11:57:33 +0200 |
paulson |
New comments on how to deal with unproved termination conditions
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:23:49 +0200 |
paulson |
Now "primes" is a set
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:44:02 +0200 |
paulson |
Renamed egcd and gcd; defined the gcd function using TFL
|
file |
diff |
annotate
|
| Fri, 14 Jun 1996 12:34:56 +0200 |
paulson |
New example of greatest common divisor
|
file |
diff |
annotate
|