src/HOL/Set.thy
Sun, 01 Jun 2025 10:29:45 +0200 haftmann another default code_unfold rule
Fri, 30 May 2025 07:47:03 +0200 haftmann qualify can_select auxiliary operations
Thu, 29 May 2025 14:17:08 +0200 haftmann annotate auxiliary operations explicitly
Wed, 28 May 2025 17:49:22 +0200 haftmann more modern qualification of auxiliary operations
Sun, 18 May 2025 14:33:01 +0000 haftmann dropped unused ML bindings
Sun, 15 Dec 2024 14:59:57 +0100 wenzelm more syntax bundles, e.g. to explore terms without notation;
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;
Fri, 22 Nov 2024 16:05:42 +0000 paulson Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique
Sat, 19 Oct 2024 19:00:19 +0200 wenzelm more type information;
Fri, 18 Oct 2024 14:20:09 +0200 wenzelm more inner-syntax markup;
Fri, 11 Oct 2024 15:17:37 +0200 wenzelm eliminate clones: just one Collect_binder_tr';
Sat, 05 Oct 2024 14:58:36 +0200 wenzelm first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
Fri, 04 Oct 2024 00:00:50 +0200 wenzelm bundles for syntax modifications seen in AFP;
Wed, 02 Oct 2024 10:34:41 +0200 wenzelm tuned markup;
Tue, 01 Oct 2024 20:39:16 +0200 wenzelm drop somewhat pointless 'syntax_consts' declarations;
Mon, 30 Sep 2024 23:32:26 +0200 wenzelm clarified syntax: use outer block (with indent);
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);
Mon, 23 Sep 2024 21:09:23 +0200 wenzelm more inner syntax markup: HOL;
Mon, 23 Sep 2024 13:32:38 +0200 wenzelm standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
Wed, 28 Aug 2024 22:54:45 +0200 wenzelm more specific "args" syntax, to support more markup for syntax consts;
Sun, 25 Aug 2024 15:16:32 +0200 wenzelm tuned whitespace;
Sun, 25 Aug 2024 15:02:19 +0200 wenzelm more markup for syntax consts;
Wed, 07 Aug 2024 15:11:54 +0200 wenzelm tuned: more antiquotations;
Fri, 02 Feb 2024 11:25:11 +0000 paulson A small number of new lemmas
Thu, 30 Nov 2023 16:56:44 +0100 nipkow added and removed [simp]s
Thu, 06 Jul 2023 16:59:12 +0100 paulson The sym_diff operator (symmetric difference)
Fri, 30 Jun 2023 08:17:27 +0200 nipkow added [simp]
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;
Tue, 02 May 2023 15:17:39 +0100 paulson More new theorems, and a necessary correction
Tue, 31 Jan 2023 14:05:16 +0000 paulson Lots more new material thanks to Manuel Eberl
Tue, 11 Oct 2022 10:45:42 +0200 nipkow moved theorem from Fun to Set
Sat, 25 Jun 2022 13:21:27 +0200 desharna moved mono and strict_mono to Fun and redefined them as abbreviations
Tue, 26 Oct 2021 11:15:40 +0100 paulson Added / moved some simple set-theoretic lemmas
Thu, 05 Aug 2021 07:12:49 +0000 haftmann clarified abstract and concrete boolean algebras
Mon, 02 Aug 2021 10:01:06 +0000 haftmann moved theory Bit_Operations into Main corpus
Tue, 11 May 2021 15:50:19 +0100 paulson Just one lemma
Sun, 28 Feb 2021 20:13:07 +0000 haftmann dissolve theory with duplicated name from afp
Sun, 15 Nov 2020 13:08:13 +0000 paulson trival
Tue, 10 Nov 2020 23:21:04 +0000 paulson cleanup
Sun, 24 May 2020 19:57:13 +0000 haftmann better closeup and more consistent terminology
Wed, 20 May 2020 15:00:25 +0100 paulson A few new theorems, plus some tidying up
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Tue, 27 Aug 2019 17:08:51 +0200 nipkow moved lemmas
Tue, 26 Mar 2019 17:01:36 +0000 paulson generalised homotopic_with to topologies; homotopic_with_canon is the old version
Thu, 21 Mar 2019 14:18:22 +0000 paulson new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
Thu, 31 Jan 2019 13:08:59 +0000 haftmann proper congruence rule for image operator
Tue, 22 Jan 2019 12:00:16 +0000 paulson renamings and new material
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 30 Dec 2018 10:34:56 +0000 haftmann prefer naming convention from datatype package for strong congruence rules
Sun, 11 Nov 2018 13:05:15 +0100 nipkow more [simp]
Wed, 31 Oct 2018 15:53:32 +0100 wenzelm clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
Sun, 21 Oct 2018 09:39:09 +0200 nipkow uniform naming of strong congruence rules
Sun, 21 Oct 2018 08:19:06 +0200 nipkow added lemma
Wed, 17 Oct 2018 14:19:07 +0100 paulson new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
Wed, 22 Aug 2018 12:32:57 +0000 haftmann new simp rule
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Thu, 11 Jan 2018 10:13:42 +0100 nipkow line break before op was intentional
less more (0) -300 -100 -60 tip