| Mon, 01 Jul 2024 12:59:46 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 10 Jun 2024 21:32:24 +0200 |
desharna |
renamed lemmas
|
file |
diff |
annotate
|
| Thu, 28 Mar 2024 09:40:58 +0100 |
desharna |
tuned proof
|
file |
diff |
annotate
|
| Wed, 06 Mar 2024 10:39:45 +0100 |
blanchet |
more multiset lemmas
|
file |
diff |
annotate
|
| Mon, 19 Feb 2024 14:31:26 +0100 |
blanchet |
remove selected occurrences of 'moura' tactic
|
file |
diff |
annotate
|
| Tue, 23 May 2023 21:43:36 +0200 |
wenzelm |
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
|
file |
diff |
annotate
|
| Wed, 10 May 2023 08:59:44 +0200 |
desharna |
added lemmas transp_on_multpHO and transp_multpHO
|
file |
diff |
annotate
|
| Wed, 10 May 2023 08:56:32 +0200 |
desharna |
tuned theory structure
|
file |
diff |
annotate
|
| Tue, 09 May 2023 22:00:36 +0200 |
desharna |
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
|
file |
diff |
annotate
|
| Mon, 08 May 2023 11:27:11 +0200 |
desharna |
added author
|
file |
diff |
annotate
|
| Mon, 08 May 2023 11:27:03 +0200 |
desharna |
added lemma asymp_on_multpHO
|
file |
diff |
annotate
|
| Mon, 08 May 2023 11:26:04 +0200 |
desharna |
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
|
file |
diff |
annotate
|
| Mon, 08 May 2023 11:16:45 +0200 |
desharna |
added lemma multpHO_implies_one_step_strong
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 14:54:03 +0200 |
desharna |
added lemmas multpHO_repeat_mset_repeat_mset[simp] and multpHO_double_double[simp]
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 15:37:17 +0100 |
desharna |
added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 12:35:37 +0100 |
desharna |
added lemma multpDM_plus_plusI[simp]
|
file |
diff |
annotate
|
| Thu, 23 Feb 2023 12:31:46 +0100 |
desharna |
added lemmas multpDM_mono_strong and multpHO_mono_strong
|
file |
diff |
annotate
|
| Sat, 18 Feb 2023 20:34:09 +0100 |
desharna |
added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO
|
file |
diff |
annotate
|
| Fri, 27 Jan 2023 12:25:36 +0100 |
desharna |
added lemma multpHO_plus_plus[simp]
|
file |
diff |
annotate
|
| Mon, 23 Jan 2023 15:11:50 +0100 |
desharna |
added lemma irreflp_on_multpHO[simp]
|
file |
diff |
annotate
|
| Mon, 23 Jan 2023 14:40:23 +0100 |
desharna |
added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and totalp_multpHO
|
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
|
| Sun, 28 Nov 2021 19:15:12 +0100 |
desharna |
added definitions multp{DM,HO} and corresponding lemmas
|
file |
diff |
annotate
|
| Sun, 28 Nov 2021 09:57:48 +0100 |
desharna |
restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3
|
file |
diff |
annotate
|
| Sat, 27 Nov 2021 10:46:57 +0100 |
desharna |
redefined less_multiset to be based on multp
|
file |
diff |
annotate
|
| Thu, 25 Nov 2021 14:02:51 +0100 |
desharna |
added asymp_{less,greater} to preorder and moved mult1_lessE out
|
file |
diff |
annotate
|
| Tue, 07 Nov 2017 15:16:40 +0100 |
blanchet |
added FIXMEs
|
file |
diff |
annotate
|
| Fri, 21 Apr 2017 21:30:48 +0200 |
blanchet |
moved lemmas from AFP to Isabelle
|
file |
diff |
annotate
|
| Thu, 16 Feb 2017 13:54:22 +0100 |
fleury |
use the cancellation simprocs directly
|
file |
diff |
annotate
|
| Mon, 13 Feb 2017 16:03:55 +0100 |
fleury |
adding simplification patterns to multiset simprocs
|
file |
diff |
annotate
|