Re: [isabelle] programmatically adding a class relation
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and