isabelle: src/HOL/Probability/Probability.thy@fd6cc1378fec (annotated)

33536 fd28b7399f2b eliminated hard tabulators; wenzelm parents: 33271 diff changeset	1	theory Probability
36080 0d9affa4e73c Added Information theory and Example: dining cryptographers hoelzl parents: 35833 diff changeset	2	imports
41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 40859 diff changeset	3	Complete_Measure
42148 d596e7bb251f rename Probability_Space to Probability_Measure hoelzl parents: 42147 diff changeset	4	Probability_Measure
42147 61d5d50ca74c add infinite product measure hoelzl parents: 41981 diff changeset	5	Infinite_Product_Measure
42861 16375b493b64 Add formalization of probabilistic independence for families of sets hoelzl parents: 42148 diff changeset	6	Independent_Family
36080 0d9affa4e73c Added Information theory and Example: dining cryptographers hoelzl parents: 35833 diff changeset	7	Information
0d9affa4e73c Added Information theory and Example: dining cryptographers hoelzl parents: 35833 diff changeset	8	"ex/Dining_Cryptographers"
41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 40859 diff changeset	9	"ex/Koepf_Duermuth_Countermeasure"
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	10	begin
7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	11	end

author	bulwahn
	Thu, 09 Jun 2011 08:32:13 +0200
changeset 43308	fd6cc1378fec
parent 42902	e8dbf90a2f3b
child 43556	0d78c8d31d0d
permissions	-rw-r--r--