src/HOL/Set.thy
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
Wed, 10 Jan 2018 18:18:34 +0100 nipkow tuned notation
Wed, 10 Jan 2018 15:21:49 +0100 nipkow Manual updates towards conversion of "op" syntax
Sun, 31 Dec 2017 21:42:20 +0000 paulson Restored correct spacing for set comprehensions
Fri, 22 Dec 2017 21:00:07 +0000 paulson new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Sun, 08 Oct 2017 22:28:20 +0200 haftmann canonical introduction and destruction rules for pairwise
Thu, 29 Sep 2016 18:52:34 +0200 hoelzl HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
Wed, 28 Sep 2016 17:01:01 +0100 paulson new material connected with HOL Light measure theory, plus more rationalisation
Thu, 22 Sep 2016 15:44:47 +0100 paulson More mainly topological results
Thu, 15 Sep 2016 14:14:49 +0100 paulson simple new lemmas, mostly about sets
Tue, 02 Aug 2016 21:05:34 +0200 wenzelm misc tuning and modernization;
Tue, 05 Jul 2016 23:39:49 +0200 wenzelm misc tuning and modernization;
Tue, 05 Jul 2016 22:23:17 +0200 wenzelm tuned;
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Sun, 19 Jun 2016 22:51:42 +0200 wenzelm misc tuning and modernization;
Tue, 14 Jun 2016 15:34:21 +0100 paulson new results about topology
Fri, 27 May 2016 23:35:13 +0200 wenzelm tuned proofs;
Mon, 23 May 2016 15:33:24 +0100 paulson Lots of new material for multivariate analysis
Tue, 17 May 2016 17:05:35 +0200 eberlm Moved material from AFP/Randomised_Social_Choice to distribution
Mon, 09 May 2016 16:02:23 +0100 paulson renamings and refinements
Mon, 18 Apr 2016 14:30:32 +0100 paulson new theorems about convex hulls, etc.; also, renamed some theorems
Mon, 04 Apr 2016 16:52:56 +0100 paulson Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
Sat, 05 Mar 2016 19:58:56 +0100 wenzelm old HOL syntax is for input only;
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Wed, 06 Jan 2016 12:18:53 +0100 hoelzl add the proof of the central limit theorem
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 26 Oct 2015 23:41:27 +0000 paulson new lemmas about topology, etc., for Cauchy integral formula
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Fri, 02 Oct 2015 15:07:41 +0100 paulson New theorems about connected sets. And pairwise moved to Set.thy.
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
less more (0) -300 -100 -60 tip