| Tue, 21 Jan 2020 11:02:27 +0100 |
Manuel Eberl |
Removed multiplicativity assumption from normalization_semidom
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:16:45 +0000 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 12:16:03 +0100 |
Manuel Eberl |
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Sun, 23 Sep 2018 15:42:19 +0200 |
nipkow |
more standard syntax
|
file |
diff |
annotate
|
| Thu, 23 Aug 2018 17:09:39 +0000 |
haftmann |
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
|
file |
diff |
annotate
|
| Thu, 23 Aug 2018 17:09:37 +0000 |
haftmann |
dropped redundant syntax translation rules for big operators
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 23:09:21 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Thu, 24 May 2018 09:26:26 +0000 |
haftmann |
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:41 +0000 |
haftmann |
tuned some proofs and added some lemmas
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:47 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid trivial definition
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| 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
|
| Fri, 18 Dec 2015 11:14:28 +0100 |
Andreas Lochbihler |
add gcd instance for integer and serialisation to target language operations
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 20:19:12 +0200 |
haftmann |
tuned facts
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
more cautious use of [iff] declarations
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:40 +0200 |
haftmann |
eliminated some duplication
|
file |
diff |
annotate
|