| Tue, 21 Jan 2020 11:02:27 +0100 |
Manuel Eberl |
Removed multiplicativity assumption from normalization_semidom
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 14:32:08 +0000 |
paulson |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
file |
diff |
annotate
|
| Sat, 19 Oct 2019 09:15:37 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
official fact collection sign_simps
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:21 +0000 |
haftmann |
removed unused fact collections
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 08:43:33 +0000 |
haftmann |
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 08:11:48 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 08:11:47 +0000 |
haftmann |
more document structure
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 08:11:46 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 09 Apr 2019 16:59:00 +0000 |
haftmann |
common type class for distributive division
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 23 May 2018 07:13:11 +0000 |
haftmann |
grouped material on numeral division
|
file |
diff |
annotate
|
| Tue, 22 May 2018 18:14:29 +0000 |
haftmann |
automatic classical rule to derive a dvd b from b mod a = 0
|
file |
diff |
annotate
|
| Tue, 22 May 2018 18:14:29 +0000 |
haftmann |
consider dvdE for automated classical proving
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 22:58:27 +0000 |
paulson |
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 08:23:19 +0100 |
eberlm |
Some lemmas on complex numbers and coprimality
|
file |
diff |
annotate
|
| Tue, 19 Dec 2017 13:58:12 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2017 17:03:20 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:44 +0000 |
haftmann |
rule out pathologic instances
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
generalized simproc
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Thu, 11 May 2017 16:47:53 +0200 |
haftmann |
more lemmas
|
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
|