| Sun, 07 Sep 2025 17:42:02 +0100 |
paulson |
Some of Wenda Li's polynomial lemmas
|
file |
diff |
annotate
|
| Sat, 06 Sep 2025 12:53:32 +0100 |
paulson |
Removed needless [simp] attribute
|
file |
diff |
annotate
|
| Fri, 05 Sep 2025 21:53:19 +0100 |
paulson |
Some lemmas moved in from Winding_Number_Eval
|
file |
diff |
annotate
|
| 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
|