#903 (Mar 29, 2019, 12:55:01 AM)

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

Started by an SCM change

This run spent:

• 5 min 0 sec waiting;
• 1 hr 12 min build duration;
• 1 hr 17 min total from scheduled to completion.