I am finding that if I give something the status of a binder
before defining the constant, so that it can be used as a
binder in the definition, the definition fails.

The error message alleges that the binder occurs freely in
the definition (which I suppose is true).

Is this a known feature?

Roger Jones

Proofpower mailing list

Reply via email to