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;