Re: [isabelle] question about locales and locale parameters

Brian Huffman wrote:
Is there any reason why "label == test.label none" could not be
implemented instead as a local *definition*? I'm thinking of how the
"def" command works within a proof script: This adds a definition that
is unfolded when the lemma is exported, but within the proof, the
simplifier just sees an opaque constant.

This unfortunately does not work in general, since "def" in proofs cannot support polymorphism.

