[isabelle-dev] Duplicate theory??

Lars Hupel hupel at in.tum.de
Mon Apr 8 18:15:56 CEST 2019


> The policy for the AFP has always been in the past: it is ok to fix
> things a few days later. Not sure why this deserves the adjective
> "catastrophic".

"catastrophic" because the failure prevented the *entire AFP* from being 
built, hence the error message.

Maybe Makarius could change that behaviour and instead of "build" 
refusing to build anything, only exclude malformed sessions.



More information about the isabelle-dev mailing list