Summary
- merged
- Hiding the constant "norm", lest it clash with the norm of a vector space
- more lemmas from Paulo
- merged
- updated for release;
- Added tag Isabelle2018-RC1 for changeset cf01d04e94d7
- fixed (?) LaTeX presentation
- merged
- Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
- more NEWS;
- tuned;
- more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
- update Sledgehammer docs w.r.t. Vampire
- added Vampire component
- added option for noncommercial Vampire