#976 (Aug 4, 2019, 12:50:06 AM)

1. more efficient data structure; (detail / hgweb)
2. clarified signature; (detail / hgweb)
3. guard constraints by record_proofs=1, until performance implications have become more clear; (detail / hgweb)
4. more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix; (detail / hgweb)
5. tuned; (detail / hgweb)
6. tuned; (detail / hgweb)
7. maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms;
   tuned; (detail / hgweb)
8. more direct proofs for type classes;
   misc tuning and cleanup; (detail / hgweb)
9. tuned; (detail / hgweb)
10. clarified modules: inference kernel maintains sort algebra within the logic; (detail / hgweb)
11. more elementary treatment of standard_vars (unconstrainT is already standard); (detail / hgweb)
12. clarified module structure; (detail / hgweb)
13. simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f); (detail / hgweb)
14. abstract type theory_id -- ensure non-equality type independently of implementation; (detail / hgweb)

Started by an SCM change

This run spent:

• 5.3 sec waiting;
• 1 hr 19 min build duration;
• 1 hr 19 min total from scheduled to completion.