src/HOL/Probability/Probability.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62083 7582b39f51ed
child 63122 dd651e3f7413
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
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@58587
    10
  Probability_Mass_Function
hoelzl@58588
    11
  Stream_Space
hoelzl@59092
    12
  Embed_Measure
hoelzl@62083
    13
  Central_Limit_Theorem
paulson@33271
    14
begin
hoelzl@47694
    15
paulson@33271
    16
end