| author | haftmann | 
| Fri, 11 Jul 2008 09:02:24 +0200 | |
| changeset 27542 | 9bf0a22f8bcd | 
| parent 21256 | 47195501ecf7 | 
| child 28529 | 7ff939586e83 | 
| permissions | -rw-r--r-- | 
| 14620 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 1 | (* Title: HOL/Import/HOL/ROOT.ML | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 2 | ID: $Id$ | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 3 | Author: Sebastian Skalberg (TU Muenchen) | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 4 | *) | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 5 | |
| 21256 | 6 | use_thy "Primes"; | 
| 17710 | 7 | setmp quick_and_dirty true use_thy "HOL4Prob"; | 
| 8 | setmp quick_and_dirty true use_thy "HOL4"; |