src/HOL/Probability/ROOT.ML
author huffman
Sat, 21 Apr 2012 10:59:52 +0200
changeset 47647 ec29cc09599d
parent 45713 badee348c5fb
permissions -rw-r--r--
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator

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