| Tue, 27 Jan 2015 16:12:40 +0100 |
hoelzl |
ereal: tuned proofs concerning continuity and suprema
|
file |
diff |
annotate
|
| Thu, 22 Jan 2015 14:51:08 +0100 |
hoelzl |
import general thms from Density_Compiler
|
file |
diff |
annotate
|
| Wed, 14 Jan 2015 10:15:41 +0100 |
Andreas Lochbihler |
allow line breaks in integral notation
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 19:10:36 +0100 |
hoelzl |
measurability prover: removed app splitting, replaced by more powerful destruction rules
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:20:14 +0100 |
hoelzl |
add congruence solver to measurability prover
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 15:47:36 +0200 |
hoelzl |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
| Tue, 03 Jun 2014 16:22:01 +0200 |
hoelzl |
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
|
file |
diff |
annotate
|
| Fri, 30 May 2014 15:56:30 +0200 |
hoelzl |
better support for restrict_space
|
file |
diff |
annotate
|
| Wed, 21 May 2014 13:52:46 +0200 |
hoelzl |
generalized Bochner integral over infinite sums
|
file |
diff |
annotate
|
| Tue, 20 May 2014 19:24:39 +0200 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
| Mon, 19 May 2014 14:26:58 +0200 |
hoelzl |
renamed positive_integral to nn_integral
|
file |
diff |
annotate
|
| Mon, 19 May 2014 13:44:13 +0200 |
hoelzl |
fixed document generation for HOL-Probability
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:04:45 +0200 |
hoelzl |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
|
file |
diff |
annotate
|