ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)

updates for jedit-4.5.0 (still inactive);

more explicit patches;

tuned comment;

removed obsolete proper_command_at (cf. 03a2dc9e0624);

added Command.proper_range (still unused);

clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;

tuned

move test targets to test target

dropped images for importer sessions

dropped dead code

more accurate dependencies

tuned ML

dropped silly code

tuned

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