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