Changes

Summary

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