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" ];