[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] consider
Hi,
I have promised to Freek the statistics about the last propositions
in "consider" items, which are immediately referenced (i.e. used in a
"by" justification). The reason why Freek asked for this, is the idea
to allow "then" or "hence" after "consider".
There are 17454 such "consider"s in the recent MML. The XPath expressions
counting it are at
http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl?view=markup,
and the line numbers for each article are at
http://kti.ms.mff.cuni.cz/~urban/Consider_results.txt .
There are 48168 "consider"s in this MML in total, and there are 33640
"consider"s which are followed by an item with a "by" justification
(this can be counted by simple modification of the above script).
So in more than a half of the relevant cases, the linking would be
"immediately" useful. Obviously. sometimes the label needs to be there,
because the "considered proposition" is referenced also later. I do not
know the number of such cases.
Best,
Josef