Summary
- 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