#987 (Aug 16, 2019, 1:15:48 AM)

1. merged (detail / hgweb)
2. more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration; (detail / hgweb)
3. more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof; (detail / hgweb)
4. support Export_Theory.read_proof, based on theory_name and serial; (detail / hgweb)
5. clarified PThm: theory_name simplifies retrieval from exports; (detail / hgweb)
6. Indexname.toString according to string_of_vname' in ML; (detail / hgweb)
7. clarified type Indexname, with plain value Int;
   eliminated pointless cache_int; (detail / hgweb)
8. more complete pattern match; (detail / hgweb)
9. export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately; (detail / hgweb)
10. support for (fully reconstructed) proof terms in Scala;
    proper cache_typs; (detail / hgweb)
11. new material; rotated premises of Lim_transform_eventually (detail / hgweb)

Started by an SCM change

This run spent:

• 25 min waiting;
• 1 hr 21 min build duration;
• 1 hr 47 min total from scheduled to completion.