| Thu, 06 Apr 2017 11:23:26 +0200 |
eberlm |
Fixed import path in Factorial_Ring
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 10:34:48 +0200 |
eberlm |
Tuned
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 21:26:25 +0100 |
haftmann |
removed dangerous simp rule: prime computations can be excessively long
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 17:57:55 +0200 |
haftmann |
more generic algebraic lemmas
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:07:39 +0200 |
fleury |
# after multiset intersection and union symbol
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 12:30:55 +0200 |
haftmann |
prefer abbreviation for trivial set conversion
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 12:30:55 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 09 Sep 2016 15:12:40 +0200 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 15:47:50 +0200 |
fleury |
add_mset constructor in multisets
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 17:47:51 +0200 |
eberlm |
is_prime -> prime
|
file |
diff |
annotate
|
| Mon, 25 Jul 2016 11:30:31 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 08:02:37 +0200 |
wenzelm |
tuned proofs -- avoid improper use of "this";
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 17:35:54 +0200 |
eberlm |
Removed redundant material related to primes
|
file |
diff |
annotate
|
| Thu, 21 Jul 2016 10:06:04 +0200 |
eberlm |
Overhaul of prime/multiplicity/prime_factors
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 15:46:52 +0200 |
eberlm |
Reformed factorial rings
|
file |
diff |
annotate
|
| Tue, 24 May 2016 18:46:51 +0200 |
eberlm |
Backed out changeset 8230358fab88
|
file |
diff |
annotate
|
| Tue, 24 May 2016 17:42:14 +0200 |
eberlm |
Deleted problematic code equation in Codegenerator_Test
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 22:44:31 +0200 |
wenzelm |
some uses of 'obtain' with structure statement;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 08:33:55 +0100 |
haftmann |
constructive formulation of factorization
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 17:53:09 +0100 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 22:44:02 +0200 |
haftmann |
formal class for factorial (semi)rings
|
file |
diff |
annotate
|