Changes

Summary

1. "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;
2. removed junk;
3. clarified diagrams;
4. clarified diagrams;
5. proper syntax diagrams; tuned whitespace;
6. tuned names;
7. tuned whitespace;
8. proper local_theory command;
9. more exports: avoid clones in AFP;
10. tuned;
11. export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files; tuned;
12. tuned whitespace;