Custom Automations in Mizar

The central aim of the Mizar project is to produce strictly formalized mathematical statements with mechanically certified proofs. When writing a Mizar formalization, a significant amount of the user's time typically goes into browsing the Mizar Mathematical Library (MML) for the already-proved results he needs. Here a few techniques to reduce this time are illustrated.