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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
