Tue, 27 Nov 2012 11:29:47 +0100 
immler 
qualified interpretation of sigma_algebra, to avoid name clashes

file 
diff 
annotate

Fri, 16 Nov 2012 18:45:57 +0100 
hoelzl 
move theorems to be more generally useable

file 
diff 
annotate

Fri, 02 Nov 2012 14:23:54 +0100 
hoelzl 
use measurability prover

file 
diff 
annotate

Fri, 02 Nov 2012 14:23:40 +0100 
hoelzl 
add measurability prover; add support for Borel sets

file 
diff 
annotate

Fri, 02 Nov 2012 14:00:39 +0100 
hoelzl 
for the product measure it is enough if only one measure is sigmafinite

file 
diff 
annotate

Thu, 11 Oct 2012 14:38:58 +0200 
hoelzl 
cleanup borel_measurable_positive_integral_(fstsnd)

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:34 +0200 
hoelzl 
induction prove for positive_integral_fst

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:27 +0200 
hoelzl 
add induction rule for intersectionstable sigmasets

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:23 +0200 
hoelzl 
remove incseq assumption from measure_eqI_generator_eq

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:18 +0200 
hoelzl 
tuned product measurability

file 
diff 
annotate

Mon, 23 Apr 2012 12:14:35 +0200 
hoelzl 
reworked Probability theory

file 
diff 
annotate

Tue, 13 Mar 2012 13:31:26 +0100 
wenzelm 
tuned proofs  eliminated pointless chaining of facts after 'interpret';

file 
diff 
annotate

Tue, 28 Feb 2012 21:53:36 +0100 
wenzelm 
avoid undeclared variables in let bindings;

file 
diff 
annotate

Wed, 07 Dec 2011 15:10:29 +0100 
hoelzl 
remove unnecessary sublocale instantiations in HOLProbability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

file 
diff 
annotate

Mon, 12 Sep 2011 07:55:43 +0200 
nipkow 
new fastforce replacing fastsimp  less confusing name

file 
diff 
annotate

Tue, 19 Jul 2011 14:36:12 +0200 
hoelzl 
Rename extreal => ereal

file 
diff 
annotate

Thu, 26 May 2011 14:12:01 +0200 
hoelzl 
add lemma sigma_sets_singleton

file 
diff 
annotate

Mon, 23 May 2011 19:21:05 +0200 
hoelzl 
move lemmas to Extended_Reals and Extended_Real_Limits

file 
diff 
annotate

Tue, 29 Mar 2011 14:27:39 +0200 
hoelzl 
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure

file 
diff 
annotate
 base
