#1014 (Sep 20, 2019, 12:50:08 AM)

1. merged (detail / hgweb)
2. clarified data structures;
   eliminated presumably obsolete check of known_theories: should be unique by construction; (detail / hgweb)
3. unused; (detail / hgweb)
4. merged (detail / hgweb)
5. Tidying and one more theorem (detail / hgweb)
6. merged (detail / hgweb)
7. explicit check of assumption prefix; (detail / hgweb)
8. clarified signature; (detail / hgweb)
9. clarified modules; (detail / hgweb)
10. support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism); (detail / hgweb)
11. proper export of result_text for 'have'; (detail / hgweb)
12. support soft types for 'assume';
    clarified "text": avoid polymorphism due to premature export; (detail / hgweb)
13. more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal); (detail / hgweb)
14. clarified modules; (detail / hgweb)
15. clarified signature -- removed unused option (see acb0807ddb56); (detail / hgweb)
16. one small last theorem (detail / hgweb)
17. Four new results from Smooth_Manifolds/Analysis_More (detail / hgweb)
18. A few more simple results (detail / hgweb)

Started by an SCM change

This run spent:

• 6.9 sec waiting;
• 1 hr 23 min build duration;
• 1 hr 23 min total from scheduled to completion.