src/HOL/Probability/ROOT.ML
author wenzelm
Fri, 08 Apr 2011 14:20:57 +0200
changeset 42287 d98eb048a2e4
parent 33615 261abc2e3155
child 45713 badee348c5fb
permissions -rw-r--r--
discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;

use_thys ["Probability"];