dropped dead code

actually add "the" Importer theory

avoid internal hol4 name references in generic importer code

generalized user-visible text

generalized attribute name

dropped dead theories

one unified Importer theory

added actual dependencies

import all importer theories in compatibility layer

merged;

dropped obsolete ROOT.ML

plugged in pre-existing theories appropriately

switch of target Import-HOL_Light-Imported: not operative at the moment

turn on quick and dirty in batch mode

tuned whitespace

file system structure separating HOL4 and HOL Light concerns

distribution of compatibility theories

formal infrastructure for import sessions

dropped dead code

tuned whitespace

spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

tuned;

tuned;

tuned;

canonical argument order for attribute application;

clarified terminology of raw protocol messages;

tuned;