| Wed, 28 May 2025 17:49:22 +0200 |
haftmann |
more modern qualification of auxiliary operations
|
file |
diff |
annotate
|
| Fri, 06 Dec 2024 20:26:33 +0100 |
wenzelm |
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
|
file |
diff |
annotate
|
| Sat, 19 Oct 2024 19:00:19 +0200 |
wenzelm |
more type information;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Tue, 08 Oct 2024 15:44:11 +0200 |
wenzelm |
tuned whitespace, to simplify hypersearch;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2024 15:36:48 +0200 |
wenzelm |
more inner syntax markup;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2024 14:23:28 +0200 |
wenzelm |
more syntax: avoid duplication in AFP;
|
file |
diff |
annotate
|
| Tue, 01 Oct 2024 20:39:16 +0200 |
wenzelm |
drop somewhat pointless 'syntax_consts' declarations;
|
file |
diff |
annotate
|
| Mon, 30 Sep 2024 23:32:26 +0200 |
wenzelm |
clarified syntax: use outer block (with indent);
|
file |
diff |
annotate
|
| Mon, 30 Sep 2024 20:30:59 +0200 |
wenzelm |
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2024 10:44:48 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Fri, 30 Aug 2024 10:16:48 +0100 |
paulson |
More tidying of old proofs
|
file |
diff |
annotate
|
| Wed, 28 Aug 2024 22:54:45 +0200 |
wenzelm |
more specific "args" syntax, to support more markup for syntax consts;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 21:10:01 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Sat, 08 Jun 2024 14:57:14 +0200 |
desharna |
renamed lemmas
|
file |
diff |
annotate
|
| Thu, 28 Mar 2024 09:41:51 +0100 |
desharna |
added special syntax for FSet.Ball and FSet.Bex
|
file |
diff |
annotate
|
| 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
|