| Wed, 07 Aug 2024 15:11:54 +0200 |
wenzelm |
tuned: more antiquotations;
|
file |
diff |
annotate
|
| Wed, 06 Mar 2024 10:39:45 +0100 |
blanchet |
more multiset lemmas
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 14:32:50 +0000 |
paulson |
Moving valuable library material from Martingales into the distribution
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 21:38:09 +0200 |
wenzelm |
tuned signature;
|
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
|
| 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, 20 Mar 2023 18:21:30 +0100 |
desharna |
added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element
|
file |
diff |
annotate
|
| Mon, 20 Mar 2023 15:02:17 +0100 |
desharna |
refactored proofs
|
file |
diff |
annotate
|
| Mon, 20 Mar 2023 15:01:59 +0100 |
desharna |
added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element
|
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
|
| Sat, 05 Nov 2022 09:57:51 +0100 |
nipkow |
Better use the finite simproc selectively only
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 14:20:07 +0100 |
nipkow |
added finite simproc
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2022 09:18:21 +0200 |
nipkow |
moved lemma fromm AFP
|
file |
diff |
annotate
|
| Mon, 17 Jan 2022 17:04:50 +0000 |
paulson |
A new lemma about inverse image
|
file |
diff |
annotate
|
| Mon, 04 Oct 2021 12:32:50 +0100 |
paulson |
new material from the Roth development, mostly about finite sets, disjoint famillies and partitions
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 18:20:13 +0100 |
paulson |
strengthened a few lemmas about finite sets and added a code equation for complex_of_real
|
file |
diff |
annotate
|
| Tue, 01 Jun 2021 19:46:34 +0200 |
nipkow |
More general fold function for maps
|
file |
diff |
annotate
|
| Mon, 03 May 2021 21:49:30 +0100 |
paulson |
A nice cardinality lemma
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 07:35:24 +0000 |
haftmann |
collected combinatorial material
|
file |
diff |
annotate
|
| Tue, 06 Oct 2020 16:55:56 +0200 |
nipkow |
added lemmas; internalized defn in class
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Thu, 06 Aug 2020 13:07:23 +0100 |
paulson |
a few more lemmas
|
file |
diff |
annotate
|
| Wed, 05 Aug 2020 19:12:08 +0100 |
paulson |
lemmas about sets and the enumerate operator
|
file |
diff |
annotate
|
| Sun, 16 Feb 2020 18:01:03 +0100 |
nipkow |
lemmas about "card A = 2"; prefer iff to implications
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 15:36:51 +0000 |
paulson |
a few new and tidier proofs (mostly about finite sets)
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 17:48:28 +0100 |
paulson |
Lindelöf spaces and supporting material
|
file |
diff |
annotate
|
| Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 14:44:52 +0000 |
paulson |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
file |
diff |
annotate
|