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

Re: [mizar] Re: Mizar 7.8.04 MML 4.80.962

Hi Josef,

>Anyway, I agree that readability is one of Mizar's
>strengths, and we should try to preserve it.

I very much agree.  (That's why I never liked the change that
you need to use "deffunc" and "defpred" now if you want to
use a scheme.  The proofs are much less readable that way.)

>>but the "identify" construction wasn't available those days.

I don't think I know what this is.  Can you clarify on the
list, or point to a description somewhere?

Freek