src/HOL/Set.thy
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;
Tue, 12 Mar 2013 07:51:10 +0100 nipkow extended set comprehension notation with {pttrn : A . P}
Tue, 05 Mar 2013 10:16:15 +0100 nipkow more lemmas about intervals
Sun, 17 Feb 2013 21:29:30 +0100 haftmann Sieve of Eratosthenes
Mon, 17 Dec 2012 17:19:21 +0100 nipkow made element and subset relations non-associative (just like all orderings)
Tue, 09 Oct 2012 16:57:58 +0200 kuncar rename Set.project to Set.filter - more appropriate name
Sat, 29 Sep 2012 18:23:46 +0200 wenzelm more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
Fri, 06 Apr 2012 19:18:00 +0200 haftmann tuned
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset
Fri, 09 Mar 2012 21:50:27 +0100 haftmann beautified
Thu, 16 Feb 2012 16:02:02 +0100 bulwahn removing unnecessary premise from diff_single_insert
Tue, 14 Feb 2012 17:11:33 +0100 wenzelm eliminated obsolete aliases;
Sat, 07 Jan 2012 20:44:23 +0100 haftmann massaging of code setup for sets
Fri, 06 Jan 2012 21:48:45 +0100 haftmann incorporated various theorems from theory More_Set into corpus
Fri, 06 Jan 2012 16:45:19 +0100 wenzelm tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);
Sun, 01 Jan 2012 15:44:15 +0100 haftmann interaction of set operations for execution and membership predicate
Sun, 01 Jan 2012 11:28:45 +0100 haftmann cleanup of code declarations
Thu, 29 Dec 2011 14:23:40 +0100 haftmann fundamental theorems on Set.bind
Thu, 29 Dec 2011 10:47:54 +0100 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
Mon, 26 Dec 2011 18:32:43 +0100 haftmann moved various set operations to theory Set (resp. Product_Type)
Sat, 24 Dec 2011 15:53:07 +0100 haftmann `set` is now a proper type constructor; added operation for set monad
Sat, 17 Dec 2011 13:08:03 +0100 wenzelm tuned signature;
Sun, 27 Nov 2011 22:03:22 +0100 wenzelm just one data slot per module;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
less more (0) -300 -100 -60 tip