Leaning Mizar

[David <lovidicus@yahoo.com>]

Hi!  I'm very interested in learning to use mizar language.... the only problem
is that I can't find any documentation on the www.mizar.org website.  The best
I could find is:

http://www.mizar.org/language/pages/mizar-article.html

Which clearly explains the 'environ' and 'begin' keywords.  But other than
that, I can't find anything else... I would like to know what the 'notation'
'constructors' 'clusters'... keywords do.  All I can find is a syntax of the
language, with no actual explanation of the items.

Also, is there an explanation of the "syntax" language?  What I can figure out
on my own is that a word followed by an equal sign introduces its definition,
words in bold are keywords that are typed out, and words in {} curly braces
seem to mean that the item can appear 0 or more times in a row.  But I would
like to have the authorative explanation of the syntax language, and not just
assume things on my own.

Thanks!!

- David

(Sorry if you receive this message twice, I couldn't figure out where I have to
send my emails to post onto the mailing list)

__________________________________________________
Do You Yahoo!?
Make international calls for as low as $.04/minute with Yahoo! Messenger
http://phonecard.yahoo.com/