another refinement chapter in the neverending numeral story

merged

observe standard conventions for doc-strings;

tuned message;

eliminated some unused Thy_Info operations;

refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;

generic external source files -- nothing special about ML here;

discontinued special treatment of ML files -- no longer complete extensions on demand;
simplified Thy_Load.check_file, with uniform error reporting;
added Thy_Load.test_file for non-strict checking;
misc tuning and simplification;

eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
reset_path is CRITICAL;

tuned signature;