src/HOL/Probability/Probability.thy
author hoelzl
Thu Jan 22 14:51:08 2015 +0100 (2015-01-22)
changeset 59425 c5e79df8cc21
parent 59092 d469103c0737
child 61359 e985b52c3eb3
permissions -rw-r--r--
import general thms from Density_Compiler
hoelzl@59092
     1
(*  Title:      HOL/Probability/Probability.thy
hoelzl@59092
     2
    Author:     Johannes Hölzl, TU München
hoelzl@59092
     3
*)
hoelzl@59092
     4
wenzelm@33536
     5
theory Probability
hoelzl@36080
     6
imports
immler@50089
     7
  Discrete_Topology
hoelzl@41689
     8
  Complete_Measure
immler@50088
     9
  Projective_Limit
hoelzl@42861
    10
  Independent_Family
hoelzl@50419
    11
  Distributions
hoelzl@58587
    12
  Probability_Mass_Function
hoelzl@58588
    13
  Stream_Space
hoelzl@59092
    14
  Embed_Measure
hoelzl@59092
    15
  Interval_Integral
hoelzl@59092
    16
  Set_Integral
hoelzl@58606
    17
  Giry_Monad
paulson@33271
    18
begin
hoelzl@47694
    19
paulson@33271
    20
end