src/HOL/Probability/ROOT.ML
author hoelzl
Fri, 03 Dec 2010 15:25:14 +0100
changeset 41023 9118eb4eb8dc
parent 33615 261abc2e3155
child 45713 badee348c5fb
permissions -rw-r--r--
it is known as the extended reals, not the infinite reals

use_thys ["Probability"];