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

Makarius makarius at sketis.net
Sun Sep 23 22:23:40 CEST 2018


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.


	Makarius


More information about the isabelle-dev mailing list