| Thu, 11 May 2017 16:47:53 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sun, 23 Apr 2017 14:53:33 +0200 |
haftmann |
include GCD as integral part of computational algebra in session HOL
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 19:13:49 +0100 |
haftmann |
gcd/lcm on finite sets
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 17:57:55 +0200 |
haftmann |
more generic algebraic lemmas
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 20:33:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 11:34:18 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2016 08:35:15 +0200 |
Manuel Eberl |
More lemmas on Gcd/Lcm
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:56:13 +0200 |
haftmann |
capitalized GCD and LCM syntax
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 22:15:09 +0100 |
Manuel Eberl |
Tuned Euclidean Rings/GCD rings
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:58 +0100 |
haftmann |
dropped various legacy fact bindings and tuned proofs
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
more sophisticated GCD syntax
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
more theorems concerning gcd/lcm/Gcd/Lcm
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
further generalization and polishing
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:37:29 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 19:23:15 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| Thu, 24 Dec 2015 09:42:49 +0100 |
haftmann |
tuned proofs and augmented lemmas
|
file |
diff |
annotate
|
| Tue, 22 Dec 2015 15:38:59 +0100 |
haftmann |
tuned proofs and augmented some lemmas
|
file |
diff |
annotate
|