| 2017-05-11 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| 2017-04-23 |
haftmann |
include GCD as integral part of computational algebra in session HOL
|
file |
diff |
annotate
|
| 2017-04-22 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| 2017-01-09 |
haftmann |
gcd/lcm on finite sets
|
file |
diff |
annotate
|
| 2016-12-17 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| 2016-10-17 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| 2016-09-18 |
haftmann |
more generic algebraic lemmas
|
file |
diff |
annotate
|
| 2016-09-18 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2016-09-15 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| 2016-07-14 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| 2016-07-01 |
Manuel Eberl |
More lemmas on Gcd/Lcm
|
file |
diff |
annotate
|
| 2016-05-25 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2016-04-18 |
haftmann |
capitalized GCD and LCM syntax
|
file |
diff |
annotate
|
| 2016-02-26 |
Manuel Eberl |
Tuned Euclidean Rings/GCD rings
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
dropped various legacy fact bindings and tuned proofs
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
more sophisticated GCD syntax
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
more theorems concerning gcd/lcm/Gcd/Lcm
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
further generalization and polishing
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| 2015-12-30 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-12-28 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-28 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| 2015-12-24 |
haftmann |
tuned proofs and augmented lemmas
|
file |
diff |
annotate
|
| 2015-12-22 |
haftmann |
tuned proofs and augmented some lemmas
|
file |
diff |
annotate
|
| 2015-12-18 |
Andreas Lochbihler |
add gcd instance for integer and serialisation to target language operations
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-11-13 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| 2015-11-09 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| 2015-11-04 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| 2015-09-13 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-07-08 |
haftmann |
tuned facts
|
file |
diff |
annotate
|
| 2015-07-08 |
haftmann |
more cautious use of [iff] declarations
|
file |
diff |
annotate
|
| 2015-07-08 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
| 2015-07-08 |
haftmann |
eliminated some duplication
|
file |
diff |
annotate
|
| 2015-07-08 |
haftmann |
more algebraic properties for gcd/lcm
|
file |
diff |
annotate
|
| 2015-06-27 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| 2015-06-27 |
haftmann |
algebraic specification for set gcd
|
file |
diff |
annotate
|
| 2015-06-25 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2015-06-17 |
wenzelm |
tuned proofs -- slightly faster;
|
file |
diff |
annotate
|
| 2015-06-02 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| 2015-04-30 |
paulson |
tidying some messy proofs
|
file |
diff |
annotate
|
| 2015-04-08 |
wenzelm |
eliminated hard tabs;
|
file |
diff |
annotate
|
| 2015-03-25 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| 2015-03-10 |
paulson |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file |
diff |
annotate
|
| 2015-02-15 |
haftmann |
explicit equivalence for strict order on lattices
|
file |
diff |
annotate
|
| 2015-02-10 |
wenzelm |
indicate slow proof (approx. 20s);
|
file |
diff |
annotate
|
| 2014-11-17 |
haftmann |
formally self-contained gcd type classes
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-10-30 |
haftmann |
more simp rules concerning dvd and even/odd
|
file |
diff |
annotate
|
| 2014-10-26 |
haftmann |
eliminated redundancies;
|
file |
diff |
annotate
|
| 2014-10-24 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file |
diff |
annotate
|
| 2014-10-23 |
haftmann |
downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| 2014-10-07 |
wenzelm |
more bibtex entries;
|
file |
diff |
annotate
|