Hi Brando,
I was trying to do the see the MML library as exercise 1.1.1 suggested from
https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz where do ppl usually check this? A local copy of it in my mizar installation or from the github page:
https://github.com/MizarSystem/MML/tree/master/mml
That document is _ancient_ (as you can also see from the
.ps.gz suffix :-)) The examples and exercises won't work at
all with the current state of the system. Recently there
have been some plans to update it, but I haven't invested
energy in that.
I don't remember why I didn't have anything about where to
look for the MML in the document. Probably it was just
sloppiness. But I certainly had the local abstr and mml
directories in mind, not anything on the web, even though web
versions (by Josef?) already existed at the time, I think.
Freek