src/HOL/Import/ROOT.ML
2010-06-02 wenzelm 2010-06-02 replaced ML pokes by explicit usedir -p; prefer -q 0 for proof terms, which avoids overhead of proof promises, while exploiting implicit parallelism of internal normalization;
2007-11-10 wenzelm 2007-11-10 qualified Proofterm.proofs;
2005-09-24 obua 2005-09-24 bug fix
2004-04-29 wenzelm 2004-04-29 removed 'constdefs' hack;
2004-04-22 wenzelm 2004-04-22 tmp hack get back to old 'constdefs';
2004-04-17 skalberg 2004-04-17 Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-02 skalberg 2004-04-02 Added HOL proof importer.