| author | haftmann | 
| Thu, 02 Dec 2010 14:34:38 +0100 | |
| changeset 40884 | 3113fd4810bd | 
| parent 37296 | 1fad5b94c0ae | 
| 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/ROOT.ML | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 2 | Author: Sebastian Skalberg (TU Muenchen) | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 3 | *) | 
| 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
 skalberg parents: 
14516diff
changeset | 4 | |
| 37296 | 5 | use_thys ["HOL4Compat", "HOL4Syntax"]; |