src/HOL/GCD.thy
6 weeks ago haftmann 2019-03-10 migrated from Nums to Zarith as library for OCaml integer arithmetic
2 months ago Manuel Eberl 2019-02-04 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
2 months ago haftmann 2019-01-31 proper congruence rule for image operator
3 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
7 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
7 months ago nipkow 2018-09-23 more standard syntax
8 months ago haftmann 2018-08-23 simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
8 months ago haftmann 2018-08-23 dropped redundant syntax translation rules for big operators
8 months ago paulson 2018-07-31 de-applying
11 months ago haftmann 2018-05-24 treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
16 months ago haftmann 2017-12-02 more simplification rules
17 months ago haftmann 2017-11-11 dedicated definition for coprimality
17 months ago haftmann 2017-10-30 tuned some proofs and added some lemmas
18 months ago haftmann 2017-10-09 tuned imports
18 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
18 months ago haftmann 2017-10-08 avoid trivial definition
18 months ago haftmann 2017-10-08 tuned proofs
23 months ago haftmann 2017-05-11 more lemmas
24 months ago haftmann 2017-04-23 include GCD as integral part of computational algebra in session HOL
24 months ago wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-01-09 haftmann 2017-01-09 gcd/lcm on finite sets
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-10-16 haftmann 2016-10-16 more standardized names
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-07-14 wenzelm 2016-07-14 misc tuning and modernization;
2016-07-01 Manuel Eberl 2016-07-01 More lemmas on Gcd/Lcm
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-04-18 haftmann 2016-04-18 capitalized GCD and LCM syntax
2016-02-26 Manuel Eberl 2016-02-26 Tuned Euclidean Rings/GCD rings
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings and tuned proofs
2016-02-17 haftmann 2016-02-17 more sophisticated GCD syntax
2016-02-17 haftmann 2016-02-17 cleansed junk-producing interpretations for gcd/lcm on nat altogether
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-02-17 haftmann 2016-02-17 more theorems concerning gcd/lcm/Gcd/Lcm
2016-02-17 haftmann 2016-02-17 further generalization and polishing
2016-02-17 haftmann 2016-02-17 pulled out legacy aliasses and infamous dvd interpretations into theory appendix
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-30 wenzelm 2015-12-30 isabelle update_cartouches -c -t;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-24 haftmann 2015-12-24 tuned proofs and augmented lemmas
2015-12-22 haftmann 2015-12-22 tuned proofs and augmented some lemmas
2015-12-18 Andreas Lochbihler 2015-12-18 add gcd instance for integer and serialisation to target language operations
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-08 haftmann 2015-07-08 tuned facts
2015-07-08 haftmann 2015-07-08 more cautious use of [iff] declarations
2015-07-08 haftmann 2015-07-08 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-07-08 haftmann 2015-07-08 eliminated some duplication
2015-07-08 haftmann 2015-07-08 more algebraic properties for gcd/lcm