changeset 39156 | b4f18ac786fa |
parent 32480 | 6c19da8e661a |
child 39616 | 8052101883c3 |
39155:3e94ebe282f1 | 39156:b4f18ac786fa |
---|---|
1 |
|
2 use_thy "~~/src/HOL/Old_Number_Theory/Primes"; |
1 use_thy "~~/src/HOL/Old_Number_Theory/Primes"; |
3 setmp_noncritical quick_and_dirty true use_thy "HOL4Prob"; |
2 setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"]; |
4 setmp_noncritical quick_and_dirty true use_thy "HOL4"; |