Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
do not import examples Probability theory
authorhoelzl
Thu, 01 Dec 2011 15:41:48 +0100
changeset 45713 badee348c5fb
parent 45712 852597248663
child 45714 ad4242285560
do not import examples Probability theory
src/HOL/Probability/Probability.thy file | annotate | diff | comparison | revisions
src/HOL/Probability/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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" ];
isabelle