[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.

Cheers
Lars



More information about the isabelle-dev mailing list