src/HOL/Import/HOL/ROOT.ML
author haftmann
Tue, 01 Sep 2009 16:00:57 +0200
changeset 32480 6c19da8e661a
parent 28529 7ff939586e83
child 39156 b4f18ac786fa
permissions -rw-r--r--
some reorganization of number theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14620
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     1
32480
6c19da8e661a some reorganization of number theory
haftmann
parents: 28529
diff changeset
     2
use_thy "~~/src/HOL/Old_Number_Theory/Primes";
28529
7ff939586e83 setmp_noncritical makes it work with future scheduler;
wenzelm
parents: 21256
diff changeset
     3
setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
7ff939586e83 setmp_noncritical makes it work with future scheduler;
wenzelm
parents: 21256
diff changeset
     4
setmp_noncritical quick_and_dirty true use_thy "HOL4";