> On 24 Sep 2018, at 6:23 am, Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
