blanchet [Sat, 27 Aug 2011 11:22:11 +0200] rev 44541
merged
blanchet [Fri, 26 Aug 2011 21:52:11 +0200] rev 44540
change default for generation of tag idempotence and tag argument equations
huffman [Fri, 26 Aug 2011 15:11:33 -0700] rev 44539
merged
huffman [Fri, 26 Aug 2011 15:11:26 -0700] rev 44538
NEWS entry for setsum_norm ~> norm_setsum
huffman [Fri, 26 Aug 2011 15:00:00 -0700] rev 44537
make HOL-Probability respect set/pred distinction
wenzelm [Fri, 26 Aug 2011 23:14:36 +0200] rev 44536
merged
huffman [Wed, 08 Sep 2010 16:10:49 -0700] rev 44535
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
huffman [Fri, 26 Aug 2011 10:38:29 -0700] rev 44534
merged
huffman [Fri, 26 Aug 2011 08:56:29 -0700] rev 44533
generalize and simplify proof of continuous_within_sequentially
huffman [Fri, 26 Aug 2011 08:12:38 -0700] rev 44532
add lemma sequentially_imp_eventually_within;
rename LIMSEQ_SEQ_conv2_lemma to sequentially_imp_eventually_at;
huffman [Thu, 25 Aug 2011 19:41:38 -0700] rev 44531
replace some continuous_on lemmas with more general versions
huffman [Thu, 25 Aug 2011 16:50:55 -0700] rev 44530
remove legacy theorem Lim_inner
huffman [Thu, 25 Aug 2011 16:42:13 -0700] rev 44529
arrange everything related to ordered_euclidean_space class together
huffman [Thu, 25 Aug 2011 16:06:50 -0700] rev 44528
generalize and shorten proof of basis_orthogonal
huffman [Thu, 25 Aug 2011 15:35:54 -0700] rev 44527
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
huffman [Thu, 25 Aug 2011 14:26:38 -0700] rev 44526
merged
huffman [Thu, 25 Aug 2011 14:25:19 -0700] rev 44525
generalize lemma finite_imp_compact_convex_hull and related lemmas
huffman [Thu, 25 Aug 2011 13:48:11 -0700] rev 44524
generalize some lemmas
huffman [Thu, 25 Aug 2011 12:52:10 -0700] rev 44523
generalize lemma convex_cone_hull
huffman [Thu, 25 Aug 2011 12:43:55 -0700] rev 44522
rename subset_{interior,closure} to {interior,closure}_mono;
remove some legacy theorem names;
huffman [Thu, 25 Aug 2011 11:57:42 -0700] rev 44521
simplify many proofs about subspace and span;
reorder premises in rule span_induct;
huffman [Thu, 25 Aug 2011 11:56:20 -0700] rev 44520
remove duplicate simp declaration
huffman [Thu, 25 Aug 2011 09:17:02 -0700] rev 44519
simplify definition of 'interior';
add lemmas interiorI and interiorE;
change lemmas interior_unique and closure_unique to rule_format;
tidy some proofs;
huffman [Wed, 24 Aug 2011 16:08:21 -0700] rev 44518
add lemma closure_union;
simplify some proofs;
huffman [Wed, 24 Aug 2011 15:32:40 -0700] rev 44517
minimize imports
huffman [Wed, 24 Aug 2011 15:06:13 -0700] rev 44516
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman [Wed, 24 Aug 2011 12:39:42 -0700] rev 44515
remove unused lemmas dimensionI, dimension_eq
huffman [Wed, 24 Aug 2011 11:56:57 -0700] rev 44514
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used