| 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:09:48 +0100 |
desharna |
tuned variable names
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 14:09:05 +0100 |
desharna |
tuned proof
|
file |
diff |
annotate
|
| Mon, 24 Mar 2025 14:08:20 +0100 |
desharna |
moved lemmas around
|
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:53:17 +0100 |
desharna |
moved lemmas around
|
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
|
| Fri, 21 Mar 2025 14:21:44 +0100 |
desharna |
added lemma trans_on_diff_Id
|
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 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
|
| Sun, 16 Mar 2025 09:11:17 +0100 |
desharna |
moved left_unique_conversep[simp] and right_unique_conversep[simp] to HOL.Relation
|
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: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: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
|
| 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
|
| Tue, 11 Mar 2025 10:20:44 +0100 |
desharna |
changed definition of refl_on
|
file |
diff |
annotate
|
| Tue, 08 Oct 2024 22:56:27 +0200 |
wenzelm |
more syntax bundles;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 21:09:23 +0200 |
wenzelm |
more inner syntax markup: HOL;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
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
|
| Mon, 20 Mar 2023 15:01:12 +0100 |
desharna |
reversed import dependency between Relation and Finite_Set; and move theorems around
|
file |
diff |
annotate
|
| Mon, 23 Jan 2023 13:31:07 +0100 |
desharna |
proper name for lemma totalp_on_total_on_eq
|
file |
diff |
annotate
|
| Fri, 13 Jan 2023 16:19:56 +0000 |
paulson |
Substantial simplification of HOL-Cardinals
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 14:34:32 +0100 |
desharna |
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 13:54:07 +0100 |
desharna |
removed old lemma names
|
file |
diff |
annotate
|
| Thu, 22 Dec 2022 21:55:51 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 16:12:17 +0100 |
desharna |
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 16:00:49 +0100 |
desharna |
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 15:54:03 +0100 |
desharna |
added lemmas trans_on_subset and transp_on_subset
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 15:52:15 +0100 |
desharna |
added lemmas trans_onD and transp_onD
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 15:41:52 +0100 |
desharna |
added lemmas trans_onI and transp_onI
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 15:36:45 +0100 |
desharna |
added lemma transp_on_trans_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 08:41:01 +0100 |
desharna |
fixed code-generation failure
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 15:33:13 +0100 |
desharna |
added predicates trans_on and transp_on and redefined trans and transp to be abbreviations
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 22:35:55 +0100 |
desharna |
added lemmas irrefl_on_if_asym_on[simp] and irreflp_on_if_asymp_on[simp]
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 12:00:15 +0100 |
desharna |
added lemmas reflI and reflD
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:44:18 +0100 |
desharna |
strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:37:03 +0100 |
desharna |
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:34:32 +0100 |
desharna |
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:30:44 +0100 |
desharna |
strengthened and renamed lemma sym_converse and added lemma symp_on_conversep
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:18:07 +0100 |
desharna |
strengthened and renamed lemmas antisymp_less and antisymp_greater
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:16:50 +0100 |
desharna |
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:14:43 +0100 |
desharna |
tuned naming
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:14:23 +0100 |
desharna |
added lemma asymp_on_asym_on_eq[pred_set_conv]
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:07:36 +0100 |
desharna |
strengthened and renamed asymp_less and asymp_greater
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:01:31 +0100 |
desharna |
added lemmas asym_on_subset and asymp_on_subset
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 08:05:23 +0100 |
desharna |
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD
|
file |
diff |
annotate
|
| Sun, 18 Dec 2022 14:03:43 +0100 |
desharna |
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 10:30:15 +0100 |
desharna |
added lemmas sym_on_subset and symp_on_subset
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 10:28:37 +0100 |
desharna |
added lemmas sym_onD and symp_onD
|
file |
diff |
annotate
|