Summary
- updated NEWS
- optimized parent computation in MaSh
- avoid loading MaSh file first time around for higher responsiveness of Sledgehammer
- tuned MaSh's metacharacters to avoid needless decoding
- optimization in MaSh parsing
- tuned ML
- removed trailing final stops in Nitpick messages
- killed final stops in Sledgehammer and friends
- tuned message
- tuning punctuation in messages output by Isabelle
- tuning whitespace in output syntax