| Thu, 04 Apr 2024 15:29:41 +0200 |
Manuel Eberl |
moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
|
file |
diff |
annotate
|
| Fri, 29 Mar 2024 19:28:59 +0100 |
Manuel Eberl |
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
|
file |
diff |
annotate
|
| Wed, 21 Feb 2024 10:46:22 +0000 |
paulson |
New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl
|
file |
diff |
annotate
|
| Fri, 28 Oct 2022 06:34:25 +0000 |
haftmann |
modulus for polynomials is invariant wrt. units
|
file |
diff |
annotate
|
| Tue, 04 Oct 2022 09:12:34 +0000 |
haftmann |
slightly less abusive proof pattern
|
file |
diff |
annotate
|
| Mon, 26 Sep 2022 08:41:53 +0000 |
haftmann |
streamlined division on polynomials
|
file |
diff |
annotate
|
| Sun, 25 Sep 2022 19:10:43 +0000 |
haftmann |
streamlined division on polynomials
|
file |
diff |
annotate
|
| Tue, 20 Sep 2022 20:12:01 +0000 |
haftmann |
streamlined division on polynomials
|
file |
diff |
annotate
|
| Mon, 12 Sep 2022 08:07:22 +0000 |
haftmann |
putting together related theorems
|
file |
diff |
annotate
|
| Fri, 24 Sep 2021 22:23:26 +0200 |
wenzelm |
tuned proofs --- avoid 'guess';
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Mon, 29 Mar 2021 12:26:13 +0100 |
paulson |
removal of needless hypothesis in hd_rev and last_rev
|
file |
diff |
annotate
|
| Sat, 09 Jan 2021 15:56:09 +0100 |
Manuel Eberl |
Corrected lemma that was too specific in HOL-Computational_Algebra
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 19:52:10 +0100 |
Manuel Eberl |
some algebra material for HOL: characteristic of a ring, algebraic integers
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 21:19:52 +0000 |
paulson |
More removal of apply
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 13:08:13 +0000 |
paulson |
trival
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:14:46 +0100 |
paulson |
tidying up some theorem statements
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 18:09:09 +0000 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
| Sun, 22 Mar 2020 19:02:39 +0000 |
paulson |
new-style Greater lemmas
|
file |
diff |
annotate
|
| Tue, 21 Jan 2020 11:02:27 +0100 |
Manuel Eberl |
Removed multiplicativity assumption from normalization_semidom
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 18:20:02 +0100 |
paulson |
removal of more redundancies, and fixes
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 13:33:50 +0000 |
haftmann |
prefer constructive primitive_part over implicit content_decompose
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 14:00:37 +0100 |
paulson |
Now based on Complex_Main, not HOL.Deriv
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:40 +0100 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 22:15:54 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
Polynomial_Factorial does not depend on Field_as_Ring as such
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 16:24:14 +0200 |
eberlm |
Some small lemmas about polynomials and FPSs
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Thu, 11 May 2017 16:47:53 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Tue, 25 Apr 2017 08:38:23 +0200 |
haftmann |
instance for polynomial rings with characteristic zero
|
file |
diff |
annotate
|
| Mon, 17 Apr 2017 16:39:01 +0200 |
haftmann |
more systematic treatment of polynomial 1
|
file |
diff |
annotate
|
| Sun, 16 Apr 2017 15:30:03 +0200 |
haftmann |
more rules concerning of_nat, of_int, numeral
|
file |
diff |
annotate
|
| Fri, 07 Apr 2017 21:17:18 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 21:37:13 +0200 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
| base
|