[isabelle-dev] Remaining uses of defer_recdef?
lp15 at cam.ac.uk
Thu Jun 11 15:26:56 CEST 2015
Absolutely, totally. We must go forward and not back.
> 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.
More information about the isabelle-dev