src/HOL/Probability/ROOT.ML

report commands as formal entities, with def/ref positions;

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