Changes

Summary

1. merged
2. tuned GUI behaviour;
3. more GUI elements;
4. clarified modules;
5. clarified process: implicit load() when finished;
6. more robust, notably initial update();
7. tuned;
8. tuned messages: implement "verbose = false", but there is no theory output anyway;
9. merged
10. added lemmas irrefl_on_subset and irreflp_on_subset
11. introduced predicates irrefl_on and irreflp_on, and redefined irrefl and irreflp as abbreviations
12. tuned messages;
13. tuned message;
14. tuned messages and options;