| Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 15:55:22 +0200 |
nipkow |
renamed multiset_of -> mset
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:29 +0200 |
hoelzl |
simplified definitions
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:29 +0200 |
hoelzl |
remove unnecessary assumption from conditional_entropy_eq
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 21:53:36 +0100 |
wenzelm |
avoid undeclared variables in let bindings;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 15:41:58 +0100 |
hoelzl |
use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 14:03:57 +0100 |
hoelzl |
moved theorems about distribution to the definition; removed oopsed-lemma
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 14:03:57 +0100 |
hoelzl |
rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
|
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
|
| Tue, 05 Apr 2011 17:10:51 +0200 |
hoelzl |
Rename extensional to extensionalD (extensional is also defined in FuncSet)
|
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, 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
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
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
|
| Wed, 01 Dec 2010 19:20:30 +0100 |
hoelzl |
Support product spaces on sigma finite measures.
|
file |
diff |
annotate
|