use_thy "~~/src/HOL/Old_Number_Theory/Primes"; setmp_noncritical quick_and_dirty true use_thy "HOL4Prob"; setmp_noncritical quick_and_dirty true use_thy "HOL4";