Changes

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

Summary

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