# HG changeset patch
# User hoelzl
# Date 1322750508 -3600
# Node ID badee348c5fb1f96ff61d3cbf22fb189acdec220
# Parent  852597248663e4f9326aa9615c1a5842edfc21c9
do not import examples Probability theory

diff -r 852597248663 -r badee348c5fb src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/Probability.thy	Thu Dec 01 15:41:48 2011 +0100
@@ -6,7 +6,5 @@
   Independent_Family
   Conditional_Probability
   Information
-  "ex/Dining_Cryptographers"
-  "ex/Koepf_Duermuth_Countermeasure"
 begin
 end
diff -r 852597248663 -r badee348c5fb src/HOL/Probability/ROOT.ML
--- a/src/HOL/Probability/ROOT.ML	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/ROOT.ML	Thu Dec 01 15:41:48 2011 +0100
@@ -1,1 +1,9 @@
-use_thys ["Probability"];
+no_document use_thys [
+  "~~/src/HOL/Library/Countable",
+  "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits",
+  "~~/src/HOL/Library/Permutation"];
+
+use_thys [
+  "Probability",
+  "ex/Dining_Cryptographers",
+  "ex/Koepf_Duermuth_Countermeasure" ];