[isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

Absolutely, totally. We must go forward and not back.
Larry

> On 11 Jun 2015, at 13:27, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> 
> 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
>