NEWS
Sat, 08 Mar 2025 22:19:49 +0100 wenzelm proper documentation for ML antiquotation \<^instantiate>;
Thu, 13 Mar 2025 14:47:56 +0100 desharna fixed NEWS
Thu, 13 Mar 2025 14:47:32 +0100 desharna added lemma quotient_disj_strong
Thu, 13 Mar 2025 10:39:41 +0100 desharna strengthened sym_trans_comp_subset
Thu, 13 Mar 2025 09:48:39 +0100 desharna added lemmas irrefl_relation_ofD, refl_relation_ofD, total_relation_ofD
Thu, 13 Mar 2025 09:41:56 +0100 desharna added lemmas antisym_relation_of[simp], asym_relation_of[simp], sym_relation_of[simp], trans_relation_of[simp]
Wed, 12 Mar 2025 19:26:59 +0100 desharna NEWS
Wed, 05 Mar 2025 08:28:21 +0100 desharna added lemmas bex_rtrancl_min_element_if_wf_on and bex_rtrancl_min_element_if_wfp_on
Tue, 04 Mar 2025 19:34:12 +0100 desharna added lemma wf_on_lex_prod[intro]
Tue, 04 Mar 2025 17:57:10 +0100 desharna added lemma wfp_on_iff_wfp
Tue, 04 Mar 2025 16:58:46 +0100 desharna added attribute "simp" to filter_mset_eq_mempty_iff
Tue, 04 Mar 2025 16:38:21 +0100 desharna removed lemma size_multiset_sum_mset[simp]
Tue, 04 Mar 2025 16:37:14 +0100 desharna added lemma size_mset_sum_mset_conv[simp] (thanks to Manuel Eberl)
Tue, 04 Mar 2025 16:07:55 +0100 desharna added lemma filter_mset_eq_mempty_iff (thanks to Manuel Eberl)
Tue, 04 Mar 2025 15:19:08 +0100 desharna renamed lemma filter_image_mset to filter_mset_image_mset
Tue, 04 Mar 2025 13:10:31 +0100 desharna added lemmas filter_mset_mono_strong, filter_mset_sum_list, set_mset_sum_list[simp] (thanks to Manuel Eberl)
Mon, 03 Mar 2025 19:52:18 +0100 wenzelm merged, resolving conflicts in src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML due to clones bb2ea9e80c33 + 62c039ce397c;
Sun, 23 Feb 2025 22:37:36 +0100 wenzelm more NEWS;
Thu, 20 Feb 2025 21:58:23 +0100 wenzelm tuned NEWS;
Wed, 19 Feb 2025 20:34:32 +0100 wenzelm more NEWS;
Tue, 25 Feb 2025 15:54:41 +0100 desharna added lemmas monotone_on_sup_fun, monotone_on_inf_fun, antimonotone_on_sup_fun, antimonotone_on_inf_fun (thanks to Alexander Pach)
Wed, 19 Feb 2025 11:11:14 +0100 wenzelm back to post-release mode -- after fork point;
Thu, 13 Feb 2025 14:26:50 +0100 wenzelm expose bundle $ISABELLE_BROWSER_INFO_LIBRARY via HTTP;
Sun, 09 Feb 2025 16:56:55 +0100 wenzelm tuned NEWS for release;
Thu, 06 Feb 2025 16:20:52 +0000 paulson Minor lemma tweaking
Mon, 03 Feb 2025 20:22:51 +0100 wenzelm merged
Mon, 03 Feb 2025 19:53:13 +0100 wenzelm tuned;
Mon, 03 Feb 2025 14:41:50 +0100 wenzelm NEWS;
Mon, 03 Feb 2025 13:17:37 +0100 desharna NEWS
Mon, 03 Feb 2025 10:46:57 +0100 desharna added lemmas ex_terminating_rtranclp_strong and ex_terminating_rtranclp
Mon, 03 Feb 2025 10:04:59 +0100 desharna added lemma strict_partial_order_wfp_on_finite_set
Sun, 02 Feb 2025 17:11:45 +0100 wenzelm tuned spelling;
Sun, 02 Feb 2025 17:05:06 +0100 wenzelm clarified NEWS: not user-relevant;
Sun, 02 Feb 2025 14:16:26 +0100 wenzelm clarified default of flatlaf.useNativeLibrary=false, for cross-platform GUI uniformity;
Sat, 01 Feb 2025 22:49:33 +0100 wenzelm merged;
Sat, 01 Feb 2025 22:41:05 +0100 wenzelm more NEWS;
Sat, 01 Feb 2025 22:13:49 +0100 wenzelm updated to flatlaf-3.5.4, with fallback on 2.6 for arm64-linux;
Sat, 01 Feb 2025 18:29:07 +0100 Fabian Huch more standard: let OS pick random port by default;
Fri, 31 Jan 2025 23:03:45 +0100 wenzelm tuned NEWS;
Fri, 31 Jan 2025 17:01:52 +0100 Lukas Stevens merged
Fri, 31 Jan 2025 16:59:12 +0100 Lukas Stevens add hook to insert premises in the order solver
Fri, 31 Jan 2025 16:23:53 +0100 wenzelm less NEWS (see also afae60d6ff15);
Wed, 08 Jan 2025 15:19:37 +0100 wenzelm switch from CVC5 to cvc5, including updates of internal tool references;
Tue, 28 Jan 2025 07:17:30 +0100 haftmann typo
Mon, 27 Jan 2025 21:31:11 +0100 wenzelm more NEWS;
Mon, 27 Jan 2025 12:13:37 +0100 wenzelm move theory "HOL-Library.Adhoc_Overloading" to Pure;
Fri, 24 Jan 2025 10:56:59 +0100 wenzelm misc tuning for release;
Fri, 24 Jan 2025 10:48:28 +0100 wenzelm more NEWS;
Fri, 24 Jan 2025 10:22:17 +0100 wenzelm merged
Thu, 23 Jan 2025 22:19:30 +0100 wenzelm support for @{instantiate (no_beta) ...};
Tue, 21 Jan 2025 17:15:52 +0100 Fabian Huch clarified find_facts URL;
Fri, 17 Jan 2025 22:38:15 +0100 wenzelm more NEWS;
Thu, 16 Jan 2025 09:26:56 +0100 haftmann theory to rewrite arithmetic operations to bit shifts
Sun, 12 Jan 2025 21:38:38 +0100 wenzelm clarified solr_data directory, provided via settings;
Sun, 12 Jan 2025 14:16:21 +0100 wenzelm clarified names;
Sun, 12 Jan 2025 13:09:42 +0100 wenzelm more NEWS + CONTRIBUTORS;
Fri, 10 Jan 2025 15:48:20 +0000 paulson fixed a typo
Thu, 09 Jan 2025 10:13:05 +0100 haftmann corrected
Mon, 23 Dec 2024 19:38:16 +0100 Lukas Bartl Rename "suggest_of" to "instantiate"
Tue, 07 Jan 2025 22:07:46 +0100 wenzelm discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
less more (0) -3000 -1000 -300 -100 -60 tip