Hi Piotr, >I was under the impression the the Encyclopaedia of >Mathematics in Mizar has been aiming, at least in part, at >this goal. EMM will mean that you will know better where to look for lemmas. But you still will need to put things like XREAL_1 in multiple directives, which still is kind of silly. So it doesn't really help with making the environ sections substantially simpler. Freek