src/HOL/Probability/Probability.thy
author haftmann
Fri Jul 04 20:18:47 2014 +0200 (2014-07-04)
changeset 57512 cc97b347b301
parent 57252 19b7ace1c5da
child 58587 5484f6079bcd
permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
wenzelm@33536
     1
theory Probability
hoelzl@36080
     2
imports
immler@50089
     3
  Discrete_Topology
hoelzl@41689
     4
  Complete_Measure
hoelzl@42148
     5
  Probability_Measure
hoelzl@42147
     6
  Infinite_Product_Measure
immler@50088
     7
  Projective_Limit
hoelzl@42861
     8
  Independent_Family
hoelzl@50419
     9
  Distributions
paulson@33271
    10
begin
hoelzl@47694
    11
paulson@33271
    12
end