src/HOL/Probability/Probability.thy
author hoelzl
Thu Oct 20 18:41:59 2016 +0200 (2016-10-20)
changeset 64320 ba194424b895
parent 64289 42f28160bad9
child 66026 704e4970d703
permissions -rw-r--r--
HOL-Probability: move stopping time from AFP/Markov_Models
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
hoelzl@63716
     7
  Central_Limit_Theorem
immler@50089
     8
  Discrete_Topology
eberlm@63194
     9
  PMF_Impl
hoelzl@63716
    10
  Projective_Limit
eberlm@63122
    11
  Random_Permutations
hoelzl@63716
    12
  SPMF
hoelzl@63716
    13
  Stream_Space
hoelzl@64283
    14
  Conditional_Expectation
hoelzl@64289
    15
  Essential_Supremum
hoelzl@64320
    16
  Stopping_Time
paulson@33271
    17
begin
hoelzl@47694
    18
paulson@33271
    19
end