| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
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
|
| 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 HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
|
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
|
| 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
|
| 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
|
| 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
|
| Thu, 02 Sep 2010 20:29:12 +0200 |
hoelzl |
Updated proofs in Dining Cryptographers theory
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 19:35:57 +0200 |
hoelzl |
Rewrite the Probability theory.
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:35:10 +0200 |
hoelzl |
Cleanup information theory
|
file |
diff |
annotate
|
| Wed, 07 Apr 2010 17:24:44 +0200 |
hoelzl |
Added Information theory and Example: dining cryptographers
|
file |
diff |
annotate
|