Summary
- merged;
- updated to 146757999c8d;
- theory Pure is default presentation context;
- clarified implicit Pure.thy;
- prefer qualified names;
- tuned;
- check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
- more operations;
- tuned;
- clarified output (see also 909dcdec2122, 34d1913f0b20);
- more operations;
- tuned;