| Thu, 12 Jun 2025 12:44:47 +0200 |
wenzelm |
discontinue old infixes;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2025 08:03:05 +0200 |
haftmann |
reorganized more code-only operations
|
file |
diff |
annotate
|
| Mon, 09 Jun 2025 22:14:38 +0200 |
haftmann |
more qualified auxiliary operations
|
file |
diff |
annotate
|
| Thu, 05 Jun 2025 15:18:27 +0000 |
haftmann |
prefer already existing operation to calculate minimum
|
file |
diff |
annotate
|
| Sun, 01 Jun 2025 20:01:22 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sun, 01 Jun 2025 16:43:09 +0200 |
wenzelm |
more generic parsing of command spans;
|
file |
diff |
annotate
|
| Sun, 01 Jun 2025 15:30:35 +0200 |
wenzelm |
support for Thy_Info.get_theories_segments, depending on system option "record_theories";
|
file |
diff |
annotate
|
| Sat, 31 May 2025 21:51:08 +0200 |
haftmann |
generic executable ranges
|
file |
diff |
annotate
|
| Fri, 30 May 2025 07:47:03 +0200 |
haftmann |
qualify can_select auxiliary operations
|
file |
diff |
annotate
|
| Thu, 29 May 2025 11:15:48 +0200 |
haftmann |
more correct language
|
file |
diff |
annotate
|
| Wed, 28 May 2025 17:49:22 +0200 |
haftmann |
more modern qualification of auxiliary operations
|
file |
diff |
annotate
|
| Wed, 21 May 2025 20:13:43 +0200 |
haftmann |
typo
|
file |
diff |
annotate
|
| Wed, 21 May 2025 14:38:46 +0200 |
wenzelm |
proper NEWS + CONTRIBUTORS;
|
file |
diff |
annotate
|
| Wed, 21 May 2025 10:30:07 +0200 |
haftmann |
disambiguate function name wrt. structures Simplifier vs. Raw_Simplifier
|
file |
diff |
annotate
|
| Tue, 20 May 2025 17:02:10 +0200 |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| Sun, 18 May 2025 14:33:01 +0000 |
haftmann |
dropped unused ML bindings
|
file |
diff |
annotate
|
| Thu, 15 May 2025 22:55:29 +0200 |
wenzelm |
explicit support for dark GUI themes in Isabelle/jEdit;
|
file |
diff |
annotate
|
| Wed, 07 May 2025 07:48:07 +0200 |
nipkow |
Kleene's fixpoint thm
|
file |
diff |
annotate
|
| Sun, 04 May 2025 15:05:51 +0200 |
haftmann |
consolidate input syntax
|
file |
diff |
annotate
|
| Wed, 23 Apr 2025 16:58:38 +0200 |
wenzelm |
update NEWS;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2025 12:27:53 +0200 |
wenzelm |
update to flatlaf-3.6, with native library support on all platforms;
|
file |
diff |
annotate
|
| Mon, 14 Apr 2025 20:19:05 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Mon, 14 Apr 2025 20:19:05 +0200 |
haftmann |
typo
|
file |
diff |
annotate
|
| Sun, 06 Apr 2025 14:21:18 +0200 |
haftmann |
use existing implementations of bit operations if nat is implemented by target-language integer
|
file |
diff |
annotate
|
| Sat, 05 Apr 2025 08:49:53 +0200 |
haftmann |
incorporate target-language integer implementation of bit shifts into Main
|
file |
diff |
annotate
|
| Fri, 04 Apr 2025 22:20:30 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 04 Apr 2025 22:20:23 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2025 11:26:40 +0200 |
desharna |
tuned NEWS
|
file |
diff |
annotate
|
| Tue, 01 Apr 2025 10:20:14 +0200 |
desharna |
tuned whitespaces
|
file |
diff |
annotate
|
| Mon, 31 Mar 2025 22:46:11 +0100 |
paulson |
Some generalisations (mostly at the level of type classes) by Alexander Pach
|
file |
diff |
annotate
|
| Tue, 25 Mar 2025 09:10:44 +0100 |
desharna |
renamed lemmas
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 14:27:18 +0100 |
desharna |
added lemmas asymp_on_mono_strong and asymp_on_mono[mono]
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 14:21:36 +0100 |
desharna |
added lemmas irreflp_on_mono_strong and irreflp_on_mono[mono]
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 14:05:55 +0100 |
desharna |
removed reflp_mono (use reflp_on_mono_strong instead)
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 14:04:11 +0100 |
desharna |
added lemma reflp_on_mono[mono]
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 13:59:08 +0100 |
desharna |
strengthened reflp_on_mono and renamed to reflp_on_mono_strong
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 09:56:20 +0100 |
desharna |
added lemmas antisymp_on_mono_stronger, antisymp_on_mono_strong, antisymp_on_mono[mono]
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 09:04:53 +0100 |
desharna |
proper lemma name
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 09:02:19 +0100 |
desharna |
added lemmas left_unique_mono_strong, left_unique_mono[mono], right_unique_mono_strong, right_unique_mono[mono]
|
file |
diff |
annotate
|
| Sun, 23 Mar 2025 15:12:20 +0100 |
wenzelm |
support for "isabelle jedit -o OPTION";
|
file |
diff |
annotate
|
| Fri, 21 Mar 2025 22:26:18 +0100 |
wenzelm |
more uniform Proof_Display.print_results for theory and proof output --- avoid loss of information seen in src/Doc/JEdit/document/output-and-state.png (the first bad changeset is f8c412a45af8, see also 53b59fa42696);
|
file |
diff |
annotate
|
| Fri, 21 Mar 2025 14:21:44 +0100 |
desharna |
added lemma trans_on_diff_Id
|
file |
diff |
annotate
|
| Thu, 20 Mar 2025 12:39:47 +0100 |
wenzelm |
ZGC of Java 21 is enabled by default: now possible, because Windows Server 2012 (vmnipkow9) has been discontinued;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2025 19:07:26 +0100 |
wenzelm |
SSH connections allow zsh as well: this happens to work with the existing Bash.char / Bach.string operations;
|
file |
diff |
annotate
|
| Mon, 17 Mar 2025 16:29:48 +0100 |
desharna |
removed lemma wf_empty (use wf_on_bot instead)
|
file |
diff |
annotate
|
| Mon, 17 Mar 2025 11:30:39 +0100 |
desharna |
added lemmas wf_on_bot[simp] and wfp_on_bot[simp]
|
file |
diff |
annotate
|
| Mon, 17 Mar 2025 09:12:18 +0100 |
desharna |
added lemmas, refl_on_top[simp], reflp_on_top[simp], sym_on_top[simp], symp_on_top[simp], trans_on_top[simp], transp_on_top[simp], total_on_top[simp], totalp_on_top[simp]
|
file |
diff |
annotate
|
| Sun, 16 Mar 2025 15:04:59 +0100 |
desharna |
removed lemmas antisym_empty[simp], antisym_bot[simp], trans_empty[simp]
|
file |
diff |
annotate
|
| Sun, 16 Mar 2025 14:51:37 +0100 |
desharna |
added lemmas antisym_on_bot[simp], asym_on_bot[simp], irrefl_on_bot[simp], sym_on_bot[simp], trans_on_bot[simp]
|
file |
diff |
annotate
|
| Sun, 16 Mar 2025 08:55:17 +0100 |
haftmann |
removed theory HOL-Library.Divides (finally)
|
file |
diff |
annotate
|
| Sun, 16 Mar 2025 09:33:17 +0100 |
desharna |
added lemmas, antisymp_on_bot[simp], asymp_on_bot[simp], irreflp_on_bot[simp], left_unique_bot[simp], symp_on_bot[simp], transp_on_bot[simp]
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 22:42:29 +0100 |
desharna |
added lemmas totalp_on_mono[mono], totalp_on_mono_strong, totalp_on_mono_stronger, totalp_on_mono_stronger_alt
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 20:33:19 +0100 |
desharna |
removed lemmas left_unique_iff and right_unique_iff
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 20:27:25 +0100 |
desharna |
added lemma left_unique_iff_Uniq
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 20:17:03 +0100 |
desharna |
Moved predicate left_unique from HOL.Transfer to HOL.Relation
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 14:29:19 +0100 |
desharna |
proper theory name in NEWS
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 14:10:23 +0100 |
desharna |
removed single_valuedp (use right_unique instead)
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 10:39:45 +0100 |
desharna |
moved predicate right_unique to theory Relation
|
file |
diff |
annotate
|
| Sat, 15 Mar 2025 09:17:46 +0100 |
desharna |
added lemma single_valuedp_eq_right_unique
|
file |
diff |
annotate
|
| Fri, 14 Mar 2025 18:13:56 +0100 |
desharna |
added lemma symp_on_equality[simp]
|
file |
diff |
annotate
|
| Fri, 14 Mar 2025 18:11:38 +0100 |
desharna |
Strengthened and renamed lemmas antisymp_equality and transp_equality
|
file |
diff |
annotate
|
| Fri, 14 Mar 2025 18:04:14 +0100 |
desharna |
strengthened lemma refl_on_empty[simp]
|
file |
diff |
annotate
|
| Fri, 14 Mar 2025 18:02:16 +0100 |
desharna |
added lemma reflp_on_refl_on_eq [pred_set_conv]
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 16:00:48 +0100 |
wenzelm |
proper document structure;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 15:49:15 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 12 Mar 2025 11:07:16 +0100 |
wenzelm |
tuned NEWS: horizontal position is treated, too;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2025 22:19:49 +0100 |
wenzelm |
proper documentation for ML antiquotation \<^instantiate>;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 14:47:56 +0100 |
desharna |
fixed NEWS
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 14:47:32 +0100 |
desharna |
added lemma quotient_disj_strong
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 10:39:41 +0100 |
desharna |
strengthened sym_trans_comp_subset
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 09:48:39 +0100 |
desharna |
added lemmas irrefl_relation_ofD, refl_relation_ofD, total_relation_ofD
|
file |
diff |
annotate
|
| 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]
|
file |
diff |
annotate
|
| Wed, 12 Mar 2025 19:26:59 +0100 |
desharna |
NEWS
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 19:34:12 +0100 |
desharna |
added lemma wf_on_lex_prod[intro]
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 17:57:10 +0100 |
desharna |
added lemma wfp_on_iff_wfp
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 16:58:46 +0100 |
desharna |
added attribute "simp" to filter_mset_eq_mempty_iff
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 16:38:21 +0100 |
desharna |
removed lemma size_multiset_sum_mset[simp]
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 16:37:14 +0100 |
desharna |
added lemma size_mset_sum_mset_conv[simp] (thanks to Manuel Eberl)
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 16:07:55 +0100 |
desharna |
added lemma filter_mset_eq_mempty_iff (thanks to Manuel Eberl)
|
file |
diff |
annotate
|
| Tue, 04 Mar 2025 15:19:08 +0100 |
desharna |
renamed lemma filter_image_mset to filter_mset_image_mset
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2025 22:37:36 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2025 21:58:23 +0100 |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2025 20:34:32 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Wed, 19 Feb 2025 11:11:14 +0100 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2025 14:26:50 +0100 |
wenzelm |
expose bundle $ISABELLE_BROWSER_INFO_LIBRARY via HTTP;
|
file |
diff |
annotate
|
| Sun, 09 Feb 2025 16:56:55 +0100 |
wenzelm |
tuned NEWS for release;
|
file |
diff |
annotate
|
| Thu, 06 Feb 2025 16:20:52 +0000 |
paulson |
Minor lemma tweaking
|
file |
diff |
annotate
|
| Mon, 03 Feb 2025 20:22:51 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 03 Feb 2025 19:53:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2025 14:41:50 +0100 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2025 13:17:37 +0100 |
desharna |
NEWS
|
file |
diff |
annotate
|
| Mon, 03 Feb 2025 10:46:57 +0100 |
desharna |
added lemmas ex_terminating_rtranclp_strong and ex_terminating_rtranclp
|
file |
diff |
annotate
|
| Mon, 03 Feb 2025 10:04:59 +0100 |
desharna |
added lemma strict_partial_order_wfp_on_finite_set
|
file |
diff |
annotate
|
| Sun, 02 Feb 2025 17:11:45 +0100 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Sun, 02 Feb 2025 17:05:06 +0100 |
wenzelm |
clarified NEWS: not user-relevant;
|
file |
diff |
annotate
|
| Sun, 02 Feb 2025 14:16:26 +0100 |
wenzelm |
clarified default of flatlaf.useNativeLibrary=false, for cross-platform GUI uniformity;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2025 22:49:33 +0100 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2025 22:41:05 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2025 22:13:49 +0100 |
wenzelm |
updated to flatlaf-3.5.4, with fallback on 2.6 for arm64-linux;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2025 18:29:07 +0100 |
Fabian Huch |
more standard: let OS pick random port by default;
|
file |
diff |
annotate
|
| Fri, 31 Jan 2025 23:03:45 +0100 |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| Fri, 31 Jan 2025 17:01:52 +0100 |
Lukas Stevens |
merged
|
file |
diff |
annotate
|
| Fri, 31 Jan 2025 16:59:12 +0100 |
Lukas Stevens |
add hook to insert premises in the order solver
|
file |
diff |
annotate
|
| Fri, 31 Jan 2025 16:23:53 +0100 |
wenzelm |
less NEWS (see also afae60d6ff15);
|
file |
diff |
annotate
|
| Wed, 08 Jan 2025 15:19:37 +0100 |
wenzelm |
switch from CVC5 to cvc5, including updates of internal tool references;
|
file |
diff |
annotate
|
| Tue, 28 Jan 2025 07:17:30 +0100 |
haftmann |
typo
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 21:31:11 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
file |
diff |
annotate
|
| Fri, 24 Jan 2025 10:56:59 +0100 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| Fri, 24 Jan 2025 10:48:28 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Fri, 24 Jan 2025 10:22:17 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 23 Jan 2025 22:19:30 +0100 |
wenzelm |
support for @{instantiate (no_beta) ...};
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 17:15:52 +0100 |
Fabian Huch |
clarified find_facts URL;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 22:38:15 +0100 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2025 09:26:56 +0100 |
haftmann |
theory to rewrite arithmetic operations to bit shifts
|
file |
diff |
annotate
|
| Sun, 12 Jan 2025 21:38:38 +0100 |
wenzelm |
clarified solr_data directory, provided via settings;
|
file |
diff |
annotate
|