#1385 (Sep 19, 2019, 5:50:22 PM)

Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

1. merged (detail / hgweb)
2. explicit check of assumption prefix; (detail / hgweb)
3. clarified signature; (detail / hgweb)
4. clarified modules; (detail / hgweb)
5. support soft types for 'have' etc., with careful export wrt. result text to avoid extra assumptions (details may differ due to polymorphism); (detail / hgweb)
6. proper export of result_text for 'have'; (detail / hgweb)
7. support soft types for 'assume';
   clarified "text": avoid polymorphism due to premature export; (detail / hgweb)
8. more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal); (detail / hgweb)
9. clarified modules; (detail / hgweb)
10. clarified signature -- removed unused option (see acb0807ddb56); (detail / hgweb)

Started by an SCM change

This run spent:

• 2 min 2 sec waiting;
• 1 hr 40 min build duration;
• 1 hr 42 min total from scheduled to completion.

• Smooth_Manifolds