Summary
- proper latex setup;
- tuned;
- abbreviations for \<nexists>;
- old HOL syntax is for input only;
- more PIDE markup;
- tuned signature -- clarified modules;
- avoid accidental handling of interrupts; interrupts have no properties;
- unused;
- tuned signature -- clarified modules;
- avoid spam in position reports;
- tuned signature;