| Mon, 06 Apr 2020 19:46:38 +0100 |
paulson |
a few more applys
|
file |
diff |
annotate
|
| Sun, 05 Apr 2020 22:04:19 +0100 |
paulson |
fixed more nasty proofs
|
file |
diff |
annotate
|
| 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
|
| Fri, 30 Dec 2016 18:02:27 +0100 |
haftmann |
more facts on sgn, abs
|
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
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
restructured matter on polynomials and normalized fractions
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 18:48:53 +0200 |
haftmann |
suitable logical type class for abs, sgn
|
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
|
| Sun, 16 Oct 2016 09:31:03 +0200 |
haftmann |
added lemma
|
file |
diff |
annotate
|
| Wed, 12 Oct 2016 20:38:47 +0200 |
haftmann |
separate type class for arbitrary quotient and remainder partitions
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
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
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 13:55:35 +0200 |
fleury |
sharing simp rules between ordered monoids and rings
|
file |
diff |
annotate
|
| Fri, 01 Jul 2016 08:35:15 +0200 |
Manuel Eberl |
More lemmas on Gcd/Lcm
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 21:40:48 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 13:57:06 +0000 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
file |
diff |
annotate
|
| Sun, 13 Mar 2016 10:22:46 +0100 |
haftmann |
more theorems on orderings
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 10:36:19 +0100 |
haftmann |
tuned bootstrap order to provide type classes in a more sensible order
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| Fri, 12 Feb 2016 16:09:07 +0100 |
hoelzl |
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
|
file |
diff |
annotate
|
| Wed, 10 Feb 2016 18:43:19 +0100 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
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 |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|