[isabelle] Nominal2 Isabelle. Default and invariants for nominal functions
I am having problems discharging the proof obligations for a nominal
function that I have written. The short sequence of 'apply's that I have
used in previous proofs, and have seen in uses of Nominal2 in the AFP, is
I notice the appearance of 'default' and 'invariant' on some nominal
functions in the AFP. I can see what the type signatures of these are and
can guess how to construct them.
My questions is: What are these used for and can they help?
This archive was generated by a fusion of
Pipermail (Mailman edition) and