clarified style: allow to search PDF for keywords containing "_";

"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; "export_code ... file" is legacy, the empty name form has been discontinued; updated examples;

removed junk;

clarified diagrams;

clarified diagrams;

proper syntax diagrams; tuned whitespace;

tuned names;

tuned whitespace;

proper local_theory command;

more exports: avoid clones in AFP;