[isabelle] size for records

Dear list,

I'm having a lot of troubles with records right now. They're not BNFs,
but luckily there's the "copy_bnf" command. Unfortunately, it seems this
doesn't generate a size function (at least I don't see it). Is it
possible to transfer the size function from the original BNF? Because
without size function, nested recursion through the record becomes tricky.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.