killed needless thm

mention docs

took out warning (BNF is still under development, but it is finished enough)

moved 'coinduction' proof method to 'HOL'

move registration of countable set type as BNF to its own theory file (+ renamed theory)

factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)

fixed LaTeX missing }

compile

support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)

tuning

NEWS;

merged

restrict node_required status and Theories panel to actual theories;

ranges of thy_load commands count as visible within perspective; convert ranges wrt. snapshot -- relevant for outdated situation;

tuned;

refer to thy_load command of auxiliary file;

proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;

load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;

tuned;

more explicit indication of missing files;

more uniform handling of inlined files;

tuned signature;

clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;

release file errors at runtime: Command.eval instead of Command.read;

maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;

always reparse nodes with thy_load commands, to update inlined files;

proper Thy_Load.append of auxiliary file names; inlined errors;

proper theory name vs. node name;