proper export of result_text for 'have';

support soft types for 'assume'; clarified "text": avoid polymorphism due to premature export;

more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);

clarified modules;

clarified signature -- removed unused option (see acb0807ddb56);

one small last theorem

Four new results from Smooth_Manifolds/Analysis_More

A few more simple results

imported new material mostly due to Sébastien Gouëzel

A couple of new theorems, stolen from AFP entries

A few new theorems, tidying up and deletion of obsolete material

merged

more errors;

clarified inversion of file name to theory name, notably for Windows;

clarified import_name: observe directory notation more strictly;

tuned signature;

clarified signature -- removed pointless operations;

clarified signature -- removed unused content;

clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);

find theories via session directories only -- ignore known_theories;

tuned;

tuned message;

merged

tuned

A little-known material, and some tidying up

merged

tuned;

clarified theory status;

dump ZF in parallel to HOL Main;

tuned messages;