use_thy "~~/src/HOL/Old_Number_Theory/Primes"; setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];