Re: where do people check for the MML library?

Hi Freek,

Interesting, so is that not the standard way to learn Mizar? I’ve been having a lot of trouble getting started so maybe I can be pointed in the right direction?

I made this post so it can be public online and avoid repetitiveness:

https://stackoverflow.com/questions/53548924/resources-to-learn-mizar-mathematical-theorem-proving-language

Regards, Brando

On Nov 29, 2018, at 4:50 PM, Freek Wiedijk <[email protected]<mailto:[email protected]>> wrote:

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