clarified signature;

more uniform thy_deps (like class_deps), see also c48d536231fe;

clarified bootstrap -- more uniform use of ML files;

prefer theory_id operations;
tuned signature;

formal Theory.check, with markup and completion;

discontinued pointless warnings: commands are only defined inside a theory context;

clarified thy_deps;