src/HOL/Set.thy
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;
Fri, 01 May 2015 08:45:30 +0200 nipkow new simp rule
Tue, 14 Apr 2015 11:32:01 +0200 Andreas Lochbihler add lemmas
Wed, 11 Feb 2015 12:01:56 +0000 paulson Merge
Tue, 10 Feb 2015 17:37:06 +0000 paulson Not a simprule, as it complicates proofs
Tue, 10 Feb 2015 16:08:11 +0000 paulson New lemmas and a bit of tidying up.
Tue, 10 Feb 2015 16:46:21 +0100 wenzelm misc tuning;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Sat, 26 Apr 2014 13:25:45 +0200 haftmann tuned
Thu, 13 Mar 2014 08:56:08 +0100 haftmann tuned proofs
Sun, 09 Mar 2014 22:45:07 +0100 haftmann tuned;
Thu, 27 Feb 2014 16:07:21 +0000 paulson A bit of tidying up
Sat, 25 Jan 2014 22:06:07 +0100 wenzelm explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
Sun, 12 Jan 2014 14:32:22 +0100 wenzelm tuned signature;
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Mon, 02 Sep 2013 17:12:59 +0200 nipkow added lemmas
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Fri, 12 Apr 2013 17:21:51 +0200 wenzelm modifiers for classical wrappers operate on Proof.context instead of claset;
less more (0) -300 -100 -60 tip