Summary
- merged
- misc tuning and modernization;
- merged
- misc tuning and modernization;
- auto indentation of quasi commands;
- tuned;
- clarified indentation (amending 37a3fc20154d);
- tuned;
- tuned;
- tuned;
- clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;
- clarified indentation: 'begin' is treated like a separate command without indent;
- tuned;
- obsolete;
- semantic indentation for unstructured proof scripts;
- misc tuning and modernization;