[isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

On 11/06/2015 14:00, Makarius wrote:
> Is that just a question of which side of the river has greener grass?

"Function" does a number of things very nicely, eg nested recursion and 
partiality. That is worth taking on board.

Tobias

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150611/f3614907/attachment.bin>