| Wed, 27 Mar 2024 15:16:09 +0000 |
paulson |
New material and a bit of refactoring
|
file |
diff |
annotate
|
| Wed, 27 Mar 2024 10:54:47 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Tue, 26 Mar 2024 09:33:33 +0100 |
desharna |
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal
|
file |
diff |
annotate
|
| Tue, 26 Mar 2024 21:25:35 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2024 21:16:47 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2024 21:09:46 +0100 |
wenzelm |
NEWS for "isabelle go_setup";
|
file |
diff |
annotate
|
| Tue, 26 Mar 2024 09:31:34 +0100 |
desharna |
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
|
file |
diff |
annotate
|
| Tue, 26 Mar 2024 06:32:38 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Mon, 25 Mar 2024 19:27:53 +0100 |
desharna |
added lemma wf_on_iff_wf
|
file |
diff |
annotate
|
| Mon, 25 Mar 2024 20:48:10 +0100 |
wenzelm |
MLton lacks arm64-linux (see also 84f2d481d6d7);
|
file |
diff |
annotate
|
| Mon, 25 Mar 2024 14:08:25 +0100 |
nipkow |
documented running time function framework by Jonas Stahl
|
file |
diff |
annotate
|
| Sat, 23 Mar 2024 18:55:38 +0100 |
desharna |
redefined wf as an abbreviation for "wf_on UNIV"
|
file |
diff |
annotate
|
| Sat, 23 Mar 2024 07:59:53 +0100 |
desharna |
tuned NEWS
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 11:24:03 +0100 |
desharna |
redefined wfP as an abbreviation for "wfp_on UNIV"
|
file |
diff |
annotate
|
| Fri, 22 Mar 2024 10:38:35 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 21:13:49 +0100 |
desharna |
added lemma wellorder.wfp_on_less[simp]
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 21:03:06 +0100 |
wenzelm |
suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
|
file |
diff |
annotate
|
| Thu, 21 Mar 2024 14:19:05 +0100 |
wenzelm |
update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin;
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 20:45:36 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 12:26:52 +0100 |
desharna |
try proof method "order" in Sledgehammer's proof reconstruction
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 11:55:58 +0100 |
desharna |
added Mirabelle action "order"
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 11:11:04 +0100 |
desharna |
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 09:26:25 +0100 |
desharna |
added lemma order_reflclp_if_transp_and_asymp
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 09:24:12 +0100 |
desharna |
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 16:05:15 +0100 |
Manuel Eberl |
more general definition of meromorphicity; Weierstraß factorisation theorem
|
file |
diff |
annotate
|
| Sun, 17 Mar 2024 19:45:07 +0100 |
desharna |
added alias wfp for wfP
|
file |
diff |
annotate
|
| Sun, 17 Mar 2024 12:34:11 +0100 |
desharna |
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
|
file |
diff |
annotate
|
| Sun, 17 Mar 2024 09:03:18 +0100 |
desharna |
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
|
file |
diff |
annotate
|
| Sat, 16 Mar 2024 09:05:17 +0100 |
desharna |
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
|
file |
diff |
annotate
|
| Fri, 15 Mar 2024 18:54:15 +0100 |
desharna |
added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
|
file |
diff |
annotate
|
| Thu, 14 Mar 2024 11:03:23 +0100 |
wenzelm |
update NEWS + CONTRIBUTORS for release;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2024 11:09:44 +0100 |
wenzelm |
update NEWS;
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 11:18:26 +0100 |
desharna |
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
|
file |
diff |
annotate
|
| Wed, 06 Mar 2024 21:52:58 +0100 |
wenzelm |
revised NEWS: OCaml / OPAM appears to be fine on arm64-linux, e.g. Ubuntu 22.04;
|
file |
diff |
annotate
|
| Wed, 06 Mar 2024 17:04:54 +0100 |
wenzelm |
update to current long-term-support version dotnet-8.0.x;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 20:25:02 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 18:42:09 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 18:41:56 +0100 |
wenzelm |
update NEWS;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 15:02:31 +0100 |
desharna |
added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp
|
file |
diff |
annotate
|
| Sun, 03 Mar 2024 12:28:22 +0100 |
wenzelm |
official support for arm64-linux, despite a few missing tools;
|
file |
diff |
annotate
|
| Fri, 01 Mar 2024 16:27:36 +0100 |
Fabian Huch |
update NEWS, following 0d7c7fe65638;
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 17:03:00 +0100 |
wenzelm |
tuned NEWS, see also c62003e05e46;
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 16:59:47 +0100 |
wenzelm |
update NEWS, following ea1913c953ef;
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 16:57:09 +0100 |
wenzelm |
tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 16:55:10 +0100 |
wenzelm |
more explicit NEWS (see 3648e9c88d0c);
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 11:12:10 +0100 |
wenzelm |
NEWS for a53287d9add3, 3e30ca77ccfe;
|
file |
diff |
annotate
|
| Wed, 28 Feb 2024 17:25:54 +0100 |
Fabian Huch |
add option for unify trace (now disabled by default as printing is excessive and rarely used);
|
file |
diff |
annotate
|
| Fri, 23 Feb 2024 09:11:31 +0100 |
blanchet |
new less ad hoc implementation of the 'moura' tactic for skolemization
|
file |
diff |
annotate
|
| Mon, 19 Feb 2024 11:39:00 +0100 |
desharna |
added lemmas relpowp_left_unique and relpow_left_unique
|
file |
diff |
annotate
|
| Mon, 19 Feb 2024 11:21:06 +0100 |
desharna |
added lemmas relpowp_right_unique and relpow_right_unique
|
file |
diff |
annotate
|
| Sat, 17 Feb 2024 16:56:55 +0100 |
wenzelm |
clarified default "isabelle build -j0 -H";
|
file |
diff |
annotate
|
| Thu, 15 Feb 2024 08:25:25 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 16:25:41 +0100 |
desharna |
added lemmas relpow_trans[trans] and relpowp_trans[trans]
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 15:33:45 +0000 |
paulson |
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
|
file |
diff |
annotate
|
| Wed, 07 Feb 2024 11:57:22 +0000 |
paulson |
NEWS: corrected the definition of convexity of functions
|
file |
diff |
annotate
|
| Mon, 05 Feb 2024 10:06:34 +0100 |
desharna |
added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult
|
file |
diff |
annotate
|
| Sat, 20 Jan 2024 20:24:04 +0100 |
wenzelm |
update to llncs-2.23;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2024 20:02:55 +0000 |
haftmann |
consolidated lemma name
|
file |
diff |
annotate
|
| Sat, 02 Dec 2023 20:49:50 +0000 |
haftmann |
compactified specification of type class parity
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 16:49:48 +0100 |
wenzelm |
removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);
|
file |
diff |
annotate
|