Changes

Summary

1. tuned declarations for more compact proof terms;
2. prefer named facts; tuned signature;
3. clarified contexts; prefer named facts;
4. tuned messages;
5. clarified command-line;
6. tuned messages;
7. tuned messages;
8. more messages -- expose potential database problems;
9. clarified errors: include stdout;
10. clarified directory;
11. tuned;
12. tuned message;
13. clarified permissions;