| Fri, 02 Jun 2023 12:14:17 +0200 |
desharna |
added lemma ffUnion_fsubset_iff
|
file |
diff |
annotate
|
| Sun, 28 May 2023 12:14:40 +0200 |
desharna |
removed intro, desc, elim, and simp annotations from FSet lemmas that are instances of lemmas in Set
|
file |
diff |
annotate
|
| Sat, 27 May 2023 23:32:40 +0200 |
desharna |
set up code generation for fset
|
file |
diff |
annotate
|
| Fri, 26 May 2023 15:44:59 +0200 |
desharna |
redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex
|
file |
diff |
annotate
|
| Fri, 26 May 2023 10:34:32 +0200 |
desharna |
renamed notin_fset to not_fmember
|
file |
diff |
annotate
|
| Fri, 26 May 2023 09:59:06 +0200 |
desharna |
added author
|
file |
diff |
annotate
|
| Fri, 26 May 2023 09:48:55 +0200 |
desharna |
renamed variables
|
file |
diff |
annotate
|
| Tue, 16 May 2023 23:41:20 +0200 |
desharna |
fixed lemma name
|
file |
diff |
annotate
|
| Tue, 16 May 2023 22:23:05 +0200 |
desharna |
redefined FSet.fmember as an abbreviation based on Set.member
|
file |
diff |
annotate
|
| Tue, 16 May 2023 14:16:20 +0200 |
desharna |
replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
|
file |
diff |
annotate
|
| Mon, 17 Oct 2022 18:21:54 +0200 |
desharna |
added lemma fmember_iff_member_fset
|
file |
diff |
annotate
|
| Thu, 13 Oct 2022 14:27:15 +0200 |
desharna |
renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset
|
file |
diff |
annotate
|
| Thu, 13 Oct 2022 10:44:27 +0200 |
desharna |
added lemma fimage_strict_mono
|
file |
diff |
annotate
|
| Wed, 12 Oct 2022 14:50:24 +0200 |
desharna |
added lemma wfP_pfsubset
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
file |
diff |
annotate
|
| Tue, 01 Jun 2021 19:46:34 +0200 |
nipkow |
More general fold function for maps
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 09:06:44 +0100 |
haftmann |
bundled syntax for state monad combinators
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 14:46:12 +0100 |
nipkow |
uniform naming
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2018 09:39:09 +0200 |
nipkow |
uniform naming of strong congruence rules
|
file |
diff |
annotate
|
| Mon, 18 Jun 2018 11:15:46 +0200 |
Lars Hupel |
material on finite sets and maps
|
file |
diff |
annotate
|
| Mon, 12 Mar 2018 20:52:53 +0100 |
Manuel Eberl |
Changes to complete distributive lattices due to Viorel Preoteasa
|
file |
diff |
annotate
|
| Sun, 04 Mar 2018 12:22:48 +0100 |
ballarin |
Drop rewrites after defines in interpretations.
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 15:27:46 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|