Josef Urban wrote: > > Besides, there are about 700000 clauses created by logically correct > generalization of all of the simple facts (simple justifications) > ever proved by Mizar, that can additionally be loaded and used in > exactly the same manner. > What you mean by 'logically correct generalization'. Binding local variables? or something more? Andrzej Trybulec