Tue, 05 Mar 2013 15:43:08 +0100 
hoelzl 
move Liminf / Limsup lemmas on complete_lattices to its own file

file 
diff 
annotate

Thu, 31 Jan 2013 11:31:30 +0100 
hoelzl 
use order topology for extended reals

file 
diff 
annotate

Tue, 04 Dec 2012 20:44:18 +0100 
hoelzl 
rules for improper Lebesgue integrals (using tendsto at_top)

file 
diff 
annotate

Wed, 28 Nov 2012 15:59:18 +0100 
wenzelm 
eliminated slightly odd identifiers;

file 
diff 
annotate

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, 16 Nov 2012 14:46:23 +0100 
hoelzl 
rules for intergration: integrating natfunctions, integrals on finite measures, constant multiplication

file 
diff 
annotate

Thu, 08 Nov 2012 11:59:48 +0100 
bulwahn 
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs

file 
diff 
annotate

Tue, 06 Nov 2012 19:18:35 +0100 
hoelzl 
add support for function application to measurability prover

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 
add syntax and a.e.rules for (conditional) probability on predicates

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:34 +0200 
hoelzl 
strong nonnegativ (instead of ae nn) for induction rule

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:33 +0200 
hoelzl 
induction prove for positive_integral_density

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:32 +0200 
hoelzl 
add induction rules for simple functions and for Borel measurable functions

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:32 +0200 
hoelzl 
introduce induction rules for simple functions and for Borel measurable functions

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:31 +0200 
hoelzl 
joint distribution of independent variables

file 
diff 
annotate

Wed, 10 Oct 2012 12:12:17 +0200 
hoelzl 
remove some unneeded positivity assumptions; generalize some assumptions to AE; tuned proofs

file 
diff 
annotate

Wed, 25 Apr 2012 19:26:00 +0200 
hoelzl 
moved lemmas to appropriate places

file 
diff 
annotate

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

file 
diff 
annotate

Tue, 13 Mar 2012 16:56:56 +0100 
wenzelm 
prefer abs_def over def_raw;

file 
diff 
annotate

Mon, 12 Mar 2012 21:41:11 +0100 
noschinl 
tuned proofs

file 
diff 
annotate

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

file 
diff 
annotate

Sat, 25 Feb 2012 09:07:41 +0100 
bulwahn 
removing unnecessary assumptions in RComplete;

file 
diff 
annotate

Fri, 04 Nov 2011 20:16:42 +0100 
wenzelm 
proper syntactic category for abstraction syntax, to avoid lowlevel exception for malformed "\<integral> x y. f \<partial>M", for example;

file 
diff 
annotate

Thu, 15 Sep 2011 12:40:08 0400 
hoelzl 
removed further legacy rules from Complete_Lattices

file 
diff 
annotate

Wed, 14 Sep 2011 10:08:52 0400 
hoelzl 
renamed Complete_Lattices lemmas, removed legacy names

file 
diff 
annotate

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

file 
diff 
annotate

Fri, 02 Sep 2011 13:57:12 0700 
huffman 
remove more duplicate lemmas

file 
diff 
annotate

Sun, 28 Aug 2011 09:20:12 0700 
huffman 
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems

file 
diff 
annotate

Thu, 21 Jul 2011 18:40:31 +0200 
haftmann 
ereal is a complete_linorder instance

file 
diff 
annotate

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

file 
diff 
annotate

Thu, 09 Jun 2011 13:55:11 +0200 
hoelzl 
jensens inequality

file 
diff 
annotate

Thu, 26 May 2011 20:51:03 +0200 
hoelzl 
integral strong monotone; finite subadditivity for measure

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, 22 Mar 2011 20:06:10 +0100 
hoelzl 
standardized headers

file 
diff 
annotate

Mon, 14 Mar 2011 14:37:49 +0100 
hoelzl 
reworked Probability theory: measures are not type restricted to positive extended reals

file 
diff 
annotate

Wed, 23 Feb 2011 11:40:12 +0100 
hoelzl 
use measure_preserving in ..._vimage lemmas

file 
diff 
annotate

Fri, 04 Feb 2011 14:16:55 +0100 
hoelzl 
add auto support for AE_mp

file 
diff 
annotate

Wed, 02 Feb 2011 12:34:45 +0100 
hoelzl 
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;

file 
diff 
annotate

Mon, 24 Jan 2011 22:29:50 +0100 
hoelzl 
use preimage measure, instead of image

file 
diff 
annotate

Fri, 14 Jan 2011 15:56:42 +0100 
hoelzl 
tuned formalization of subalgebra

file 
diff 
annotate

Fri, 14 Jan 2011 14:21:48 +0100 
hoelzl 
introduced integral syntax

file 
diff 
annotate

Wed, 08 Dec 2010 19:32:11 +0100 
hoelzl 
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand

file 
diff 
annotate

Wed, 08 Dec 2010 16:15:14 +0100 
hoelzl 
integral over setprod

file 
diff 
annotate

Wed, 08 Dec 2010 16:15:14 +0100 
hoelzl 
cleanup bijectivity btw. product spaces and pairs

file 
diff 
annotate

Mon, 06 Dec 2010 19:54:56 +0100 
hoelzl 
folding on arbitrary Lebesgue integrable functions

file 
diff 
annotate

Fri, 03 Dec 2010 15:25:14 +0100 
hoelzl 
it is known as the extended reals, not the infinite reals

file 
diff 
annotate

Thu, 02 Dec 2010 15:09:02 +0100 
hoelzl 
generalized simple_functionD

file 
diff 
annotate

Thu, 02 Dec 2010 14:57:21 +0100 
hoelzl 
Shorter definition for positive_integral.

file 
diff 
annotate

Thu, 02 Dec 2010 14:34:58 +0100 
hoelzl 
Move SUP_commute, SUP_less_iff to HOL image;

file 
diff 
annotate

Wed, 01 Dec 2010 21:03:02 +0100 
hoelzl 
Generalized simple_functionD and less_SUP_iff.

file 
diff 
annotate

Wed, 01 Dec 2010 19:20:30 +0100 
hoelzl 
Support product spaces on sigma finite measures.

file 
diff 
annotate

Sun, 28 Nov 2010 15:20:51 +0100 
nipkow 
gave more standard finite set rules simp and intro attribute

file 
diff 
annotate

Fri, 01 Oct 2010 16:05:25 +0200 
haftmann 
constant `contents` renamed to `the_elem`

file 
diff 
annotate

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

file 
diff 
annotate

Tue, 07 Sep 2010 10:05:19 +0200 
nipkow 
expand_fun_eq > ext_iff

file 
diff 
annotate

Thu, 02 Sep 2010 17:12:40 +0200 
hoelzl 
move lemmas to correct theory files

file 
diff 
annotate

Tue, 24 Aug 2010 14:41:37 +0200 
hoelzl 
moved generic lemmas in Probability to HOL

file 
diff 
annotate
