Changes

Summary

1. redundant;
2. allow cartouche within ML string;
3. verbatim output consists of plain lines;
4. old-style inner comments are legacy;
5. more markup: disable spell-checker for raw latex;
6. clarified signature: items with \isasep are special;
7. clarified signature;
8. tuned message;
9. clarified operations;
10. tuned signature: removed unused operations;
11. tuned: prefer list operations over Source.source; approximative parsing of theory header;
12. tuned: prefer list operations over Source.source;
13. tuned: prefer list operations over Source.source;
14. clarified signature;
15. clarified position;
16. clarified operations;