src/HOL/Import/HOL/ROOT.ML
changeset 28529 7ff939586e83
parent 21256 47195501ecf7
child 32480 6c19da8e661a
equal deleted inserted replaced
28528:0cf2749e8ef7 28529:7ff939586e83
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     4 *)
     5 
     5 
     6 use_thy "Primes";
     6 use_thy "Primes";
     7 setmp quick_and_dirty true use_thy "HOL4Prob";
     7 setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
     8 setmp quick_and_dirty true use_thy "HOL4";
     8 setmp_noncritical quick_and_dirty true use_thy "HOL4";