> Incompleteness FAILED This problem has already been addressed. Makarius changed some Isabelle signatures in Isabelle/4d04e14d7ab8, and adapted AFP in d46ea7497f. Unfortunately it's currently impossible to perform atomic changes to both repositories. Cheers Lars