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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and