src/HOL/Multivariate_Analysis/Integration.thy
Sat, 25 May 2013 15:44:29 +0200 haftmann weaker precendence of syntax for big intersection and union on sets
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
Tue, 26 Mar 2013 12:20:52 +0100 hoelzl separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Tue, 05 Mar 2013 15:43:19 +0100 hoelzl move lemma Inf to usage point
Thu, 17 Jan 2013 15:17:48 +0100 wenzelm tuned proofs;
Wed, 16 Jan 2013 22:18:13 +0100 wenzelm tuned proofs;
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Tue, 04 Dec 2012 18:00:40 +0100 hoelzl remove SMT proofs in Multivariate_Analysis
Wed, 28 Nov 2012 15:59:18 +0100 wenzelm eliminated slightly odd identifiers;
Tue, 27 Nov 2012 13:22:29 +0100 wenzelm eliminated some improper identifiers;
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Thu, 01 Nov 2012 13:32:57 +0100 blanchet regenerated SMT certificates
Mon, 22 Oct 2012 17:09:49 +0200 wenzelm tuned proofs;
Thu, 04 Oct 2012 11:45:56 +0200 wenzelm tuned proofs;
Mon, 01 Oct 2012 17:29:00 +0200 wenzelm tuned proofs;
Fri, 07 Sep 2012 15:15:07 +0200 wenzelm tuned proofs;
Fri, 07 Sep 2012 13:58:43 +0200 wenzelm tuned proofs;
Mon, 04 Jun 2012 09:07:23 +0200 boehmes restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
Tue, 03 Apr 2012 15:15:00 +0200 huffman modernized obsolete old-style theory name with proper new-style underscore
Tue, 27 Mar 2012 16:59:13 +0300 blanchet renamed "smt_fixed" to "smt_read_only_certificates"
Tue, 13 Mar 2012 16:56:56 +0100 wenzelm prefer abs_def over def_raw;
Tue, 27 Dec 2011 09:45:10 +0100 haftmann be explicit about Finite_Set.fold
Mon, 12 Sep 2011 11:39:29 -0700 huffman simplify proofs using LIMSEQ lemmas
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Thu, 25 Aug 2011 12:43:55 -0700 huffman rename subset_{interior,closure} to {interior,closure}_mono;
Wed, 24 Aug 2011 11:56:57 -0700 huffman move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Fri, 12 Aug 2011 20:55:22 -0700 huffman remove redundant lemma setsum_norm in favor of norm_setsum;
Fri, 12 Aug 2011 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Thu, 11 Aug 2011 14:24:05 -0700 huffman avoid duplicate rule warnings
Wed, 10 Aug 2011 16:35:50 -0700 huffman remove several redundant and unused theorems about derivatives
Tue, 09 Aug 2011 10:30:00 -0700 huffman mark some redundant theorems as legacy
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Fri, 20 May 2011 08:16:56 +0200 haftmann use point-free characterization for locale fun_left_comm_idem
Mon, 14 Mar 2011 14:37:33 +0100 hoelzl moved t2_spaces to HOL image
Sun, 13 Mar 2011 22:24:10 +0100 wenzelm eliminated hard tabs;
Thu, 03 Mar 2011 10:55:41 +0100 hoelzl finally remove upper_bound_finite_set
Mon, 28 Feb 2011 22:10:57 +0100 boehmes removed dependency on Dense_Linear_Order
Fri, 25 Feb 2011 22:07:56 +0100 nipkow got rid of lemma upper_bound_finite_set
Mon, 17 Jan 2011 17:45:52 +0100 boehmes made Z3 the default SMT solver again
Thu, 06 Jan 2011 17:51:56 +0100 boehmes differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Fri, 12 Nov 2010 15:56:07 +0100 boehmes look for certificates relative to the theory
Tue, 26 Oct 2010 11:46:19 +0200 boehmes changed SMT configuration options; updated SMT certificates
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Mon, 23 Aug 2010 19:35:57 +0200 hoelzl Rewrite the Probability theory.
Thu, 01 Jul 2010 11:48:42 +0200 hoelzl Add theory for indicator function.
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Tue, 11 May 2010 19:21:05 +0200 hoelzl Removed usage of normalizating locales.
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Fri, 07 May 2010 09:59:24 +0200 haftmann prefix normalizing replaces class_semiring
Wed, 28 Apr 2010 22:20:59 -0700 huffman remove redundant lemma vector_dist_norm
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:21:25 -0700 huffman fix lots of looping simp calls and other warnings
Sun, 25 Apr 2010 16:23:40 -0700 huffman generalize type of continuous_on
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
less more (0) -60 tip