Re: RE[mizar] LPREM,RELINFER and *603,*604,*605

[rk1 <rkam2001@hotmail.com>]

Thank you for the fast and comprehensive response.  I understand better how
to properly use RELPREM now since you pointed out that I should be looking
at 'then' linkings when I see a *603.

RELINFER, however, gives me over 400 errors in my file.  Thanks to your
example, now I see what all those errors mean: my style of proof writing is
rather "incremental" and I like to use one fact at a time to go from one
statement to the next.  You and RELINFER are telling me I can condense many
of these incremental groups of statements into single steps.

Do I absolutely have to remove all the RELINFER *604 and *605 errors to
prepare my file for submission to the MML?  I removed all the *602 and *603
from RELPREM as I agree those make my proof clearer, but I think condensing
many of my chosen steps as RELINFER suggests would make my proof harder to
read.
-- 
View this message in context: http://www.nabble.com/RELPREM%2CRELINFER-and-*603%2C*604%2C*605-tp14544828p14545328.html
Sent from the Mizar mailing list archive at Nabble.com.