| Fri, 30 Sep 2016 16:08:38 +0200 |
hoelzl |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 23:03:27 +0200 |
hoelzl |
Probability: show that measures form a complete lattice
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Mon, 04 May 2015 17:35:31 +0200 |
hoelzl |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 12:06:18 +0100 |
hoelzl |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
|
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
|
| Tue, 07 Oct 2014 10:48:29 +0200 |
hoelzl |
move Stream theory from Datatype_Examples to Library
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 10:34:24 +0200 |
hoelzl |
add Giry monad
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 16:27:31 +0200 |
hoelzl |
add measure space for (coinductive) streams
|
file |
diff |
annotate
|