Re: [isabelle] programmatically adding a class relation



Makarius wrote:

AxClass.add_classrel refers to Logic.dest_classrel internally, which expectes results in canonical form, with generalized variables. In contrast Logic.mk_classrel produces a fixed form, because this is what you need during the proof.

Normally the system converts between fixed and arbitrary variables transparently, but this requires use of higher-level goal interfaces rather than Goal.prove_raw. See AxClass.prove_classrel (in src/Pure/axclass.ML) of how to do something like that.

Thanks.  Indeed, I should have been using prove_classrel all along.

Michael.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.