| Mon, 09 Jun 2025 22:14:38 +0200 |
haftmann |
more qualified auxiliary operations
|
file |
diff |
annotate
|
| Wed, 21 May 2025 21:48:42 +0200 |
Manuel Eberl |
three lemmas for HOL-Complex_Analysis, HOL-Computational_Algebra
|
file |
diff |
annotate
|
| Sun, 16 Feb 2025 11:57:33 +0000 |
paulson |
A few lemmas brought in from Polynomial_Interpolation
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Wed, 16 Oct 2024 20:22:20 +0200 |
wenzelm |
redundant;
|
file |
diff |
annotate
|
| Tue, 01 Oct 2024 20:39:16 +0200 |
wenzelm |
drop somewhat pointless 'syntax_consts' declarations;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2024 23:32:26 +0200 |
wenzelm |
clarified syntax: use outer block (with indent);
|
file |
diff |
annotate
|
| Mon, 30 Sep 2024 20:30:59 +0200 |
wenzelm |
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2024 22:54:45 +0200 |
wenzelm |
more specific "args" syntax, to support more markup for syntax consts;
|
file |
diff |
annotate
|
| 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
|