[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] relinfer

To: Mizar-Forum <mizar-forum@mizar.uwb.edu.pl>
Subject: [mizar] relinfer
From: Artur Kornilowicz <arturk@math.uwb.edu.pl>
Date: Wed, 18 Jun 2003 21:50:26 +0200 (CEST)

Dear All,

after some discussions on necessity of removing all errors (warnings)
reported by RELINFER (a Mizar tool marking irrelevant inferences in Mizar
articles) we decided to realize a revision of the MML, which automatically
removes all such cases from the MML.

Some results:

total number of all warnings: 39315, where 1546 in the article with the
greatest number of warnings

size of the MML:
- before the revision: 58713600
- after:               58017280

Then 696320 (1.2%) bytes have been removed.

With regards
Artur Kornilowicz

Prev by Date: [mizar] New Mizar articles
Next by Date: [mizar] Proposal for binders in Mizar
Index(es):
- Chronological
- Thread