[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
not working.

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 MHonArc.