src/HOL/Multivariate_Analysis/Integration.thy
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
less more (0) -15 tip