LIMSEQ_def -> LIMSEQ_iff

generalize constants in SEQ.thy to class metric_space

early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap; late setup of ML_Env and ML_Compiler;

structure ML_Compiler;

added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);

added flatten;

tuned signature;

export secure_mltext;

tuned comments;

maintain tokens within common ML environment;

ML_Env;

slightly later setup of ML and secure operations;

moved local ML environment to separate module ML_Env;

removed print function from global ML name space, to reduce risk of surprises;

made SML/NJ happy;

attempt to eliminate adhoc makestring at runtime (which is not well-defined);

eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;

provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;

no longer open PolyML -- to avoid surprises within the global name space; recovered some important PolyML bindings (NB: print and makestring cannot be rebound without loosing infinite overloading);

explicit PolyML qualification;

removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;

test experimental Poly/ML 5.3;

removed obsolete COPYDB flag;

explicit PolyML.install_pp;

renamed polyml_pp.ML to pp_polyml.ML; explicit PolyML.install_pp;

more modular setup of runtime compilation;

more precise version information;

uniform treatment of shellscript mode;

updated example settings;

discontinued support for Poly/ML 4.x versions;

ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");

eliminated old Attrib.add_attributes (and Attrib.syntax);