src/HOL/Probability/ROOT.ML
author hoelzl
Thu Dec 01 15:41:48 2011 +0100 (2011-12-01)
changeset 45713 badee348c5fb
parent 33615 261abc2e3155
permissions -rw-r--r--
do not import examples Probability theory
hoelzl@45713
     1
no_document use_thys [
hoelzl@45713
     2
  "~~/src/HOL/Library/Countable",
hoelzl@45713
     3
  "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits",
hoelzl@45713
     4
  "~~/src/HOL/Library/Permutation"];
hoelzl@45713
     5
hoelzl@45713
     6
use_thys [
hoelzl@45713
     7
  "Probability",
hoelzl@45713
     8
  "ex/Dining_Cryptographers",
hoelzl@45713
     9
  "ex/Koepf_Duermuth_Countermeasure" ];