| 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
|
| Thu, 20 Jul 2017 17:13:17 +0200 |
Lars Hupel |
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 09:31:36 +0200 |
Lars Hupel |
card_0_eq ~> fcard_0_eq
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 09:22:14 +0200 |
Lars Hupel |
material from $AFP/Formula_Derivatives/FSet_More
|
file |
diff |
annotate
|
| Mon, 10 Jul 2017 18:53:38 +0200 |
Lars Hupel |
finite sets are countable
|
file |
diff |
annotate
|
| Mon, 10 Jul 2017 16:38:42 +0200 |
Lars Hupel |
lift sum to finite sets
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 14:50:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 06 Aug 2016 13:36:49 +0200 |
Lars Hupel |
some additions to FSet
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 09:44:16 +0200 |
hoelzl |
move Conditional_Complete_Lattices to Main
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:31 +0100 |
blanchet |
nicer 'Spec_Rules' for size function
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Sun, 12 Jul 2015 13:04:42 +0200 |
Lars Hupel |
Quickcheck setup for finite sets
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
tuned proof; forget the transfer rule for size_fset
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
merged two small theory files
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
localize new size function generation code
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
added 'size' of finite sets
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:32 +0200 |
kuncar |
simplify and fix theories thanks to 356a5efdb278
|
file |
diff |
annotate
|