The following page contains all the definitions from first 10 MML articles in order of processing (see mml.lar file in Mizar distribution). It seems to be a good way to get first impression on mathematics in Mizar system.

http://myjavaserver.com/~michael137/definitions.html

-- MichaelNedzelsky - 31 Jul 2005

---

To get similar result with MML Query browser it is enough to write the following template and then press GET button. (See also http://merak.pb.bialystok.pl/mmlquery/getdata.php)

<mmlq type="force" properties="on" label="on"/> <mmlq type="foreach" query="list of article ordered by processing order select 0-9"> <hr>---------- <mmlq type="value" style="u-q"/> ----------<br> :: <mmlq type="title"/><br> :: by <mmlq type="author"/><hr> <mmlq type="foreach" operation="all notat"> <mmlq type="explain"/> <hr width="20%" align="left"> </mmlq></mmlq>

To get definitions from different amount of articles change "select 0-9". To get theorems change "all notat" to "all th".

-- GrzegorzBancerek - 10 Dec 2005
to top