| Wed, 05 Apr 2017 13:47:41 +0200 |
haftmann |
more concise criterion
|
file |
diff |
annotate
|
| Wed, 05 Apr 2017 13:47:40 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 11:52:28 +0200 |
wenzelm |
proper imports;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 23:00:11 +0100 |
haftmann |
generalized definition
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 19:13:49 +0100 |
haftmann |
gcd/lcm on finite sets
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 18:53:06 +0100 |
haftmann |
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 17:11:21 +0100 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 14:49:21 +0100 |
haftmann |
lead_coeff is more appropriate as abbreviation
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:28 +0100 |
haftmann |
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
|
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 11:46:22 +0200 |
nipkow |
setsum -> sum
|
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
|
| Wed, 12 Oct 2016 20:38:47 +0200 |
haftmann |
separate type class for arbitrary quotient and remainder partitions
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 11:24:36 +0100 |
paulson |
Generalised the type of map_poly
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 12:30:55 +0200 |
haftmann |
prefer abbreviation for trivial set conversion
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 15:12:40 +0200 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 21:28:55 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2016 17:17:23 +0200 |
Manuel Eberl |
Deprivatisation of lemmas in Polynomial_Factorial
|
file |
diff |
annotate
|
| Tue, 16 Aug 2016 12:41:43 +0200 |
eberlm |
Polynomial algebra cleanup (tuned)
|
file |
diff |
annotate
|
| Tue, 16 Aug 2016 12:02:09 +0200 |
eberlm |
Polynomial algebra cleanup
|
file |
diff |
annotate
| base
|