isabelle: src/HOL/Probability/Probability.thy@500ef036117b (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
50089 1badf63e5d97 generalized to copy of countable types instead of instantiation of nat for discrete topology immler parents: 50088 diff changeset	3	Discrete_Topology
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	4	Complete_Measure
42148 d596e7bb251f rename Probability_Space to Probability_Measure hoelzl parents: 42147 diff changeset	5	Probability_Measure
42147 61d5d50ca74c add infinite product measure hoelzl parents: 41981 diff changeset	6	Infinite_Product_Measure
50088 32d1795cc77a added projective limit; immler parents: 50087 diff changeset	7	Projective_Limit
42861 16375b493b64 Add formalization of probabilistic independence for families of sets hoelzl parents: 42148 diff changeset	8	Independent_Family
36080 0d9affa4e73c Added Information theory and Example: dining cryptographers hoelzl parents: 35833 diff changeset	9	Information
50419 3177d0374701 add exponential and uniform distributions hoelzl parents: 50089 diff changeset	10	Distributions
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	11	begin
47694 05663f75964c reworked Probability theory hoelzl parents: 45713 diff changeset	12
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: diff changeset	13	end

author	blanchet
	Mon, 20 Jan 2014 21:45:08 +0100
changeset 55086	500ef036117b
parent 50419	3177d0374701
child 57252	19b7ace1c5da
permissions	-rw-r--r--