[isabelle-dev] popup in ce6320b9ef9b

Lars Hupel hupel at in.tum.de
Thu Nov 19 11:41:08 CET 2015

> Here is a minimal example, but I am at loss to explain what is going on
> here.

The usual reason for a term being annotated twice is that it is (type)
checked twice.


More information about the isabelle-dev mailing list