[isabelle-dev] function (default) is legacy feature (since 2010)

[Gerwin.Klein at data61.csiro.au]

> On 24 Sep 2018, at 6:23 am, Makarius <makarius at sketis.net> wrote:
> 
> Are there any remaining uses of "function (default)"?
> 
> changeset:   41417:211dbd42f95d
> parent:      41414:00b2b6716ed8
> user:        krauss
> date:        Wed Dec 29 21:52:41 2010 +0100
> function (default) is legacy feature
> 
> 
> I don't see any remaining applications in Isabelle + AFP. So it looks
> like we can just remove it without further ado.

Confirming that this would also be safe from our side.

Cheers,
Gerwin