| Tue, 04 Apr 2017 10:34:48 +0200 |
eberlm |
Tuned
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
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
|
| 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:29 +0100 |
haftmann |
moved euclidean ring to HOL
|
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:14 +0100 |
haftmann |
more fine-grained type class hierarchy for div and mod
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
eliminated irregular aliasses
|
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 21:48:52 +0200 |
haftmann |
more standard naming convention
|
file |
diff |
annotate
|
| Wed, 12 Oct 2016 20:38:47 +0200 |
haftmann |
separate type class for arbitrary quotient and remainder partitions
|
file |
diff |
annotate
|
| Tue, 11 Oct 2016 16:44:13 +0200 |
haftmann |
stripped dependency on pragmatic type class semiring_div
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 17:57:55 +0200 |
haftmann |
more generic algebraic lemmas
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 17:47:51 +0200 |
eberlm |
is_prime -> prime
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 15:46:52 +0200 |
eberlm |
Reformed factorial rings
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Sun, 28 Feb 2016 21:19:58 +0100 |
Manuel Eberl |
Minor adjustments to euclidean rings
|
file |
diff |
annotate
|
| Sun, 28 Feb 2016 12:05:52 +0100 |
Manuel Eberl |
More efficient Extended Euclidean Algorithm
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 22:15:09 +0100 |
Manuel Eberl |
Tuned Euclidean Rings/GCD rings
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 18:33:01 +0100 |
Manuel Eberl |
Fixed code equations for Gcd/Lcm
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 14:58:07 +0100 |
eberlm |
Tuned Euclidean Ring instance for polynomials
|
file |
diff |
annotate
|
| Thu, 25 Feb 2016 16:44:53 +0100 |
eberlm |
Tuned Euclidean 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 |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 20:19:12 +0200 |
haftmann |
tuned facts
|
file |
diff |
annotate
|