[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

Makarius makarius at sketis.net
Fri Sep 13 23:09:06 CEST 2013


On Fri, 13 Sep 2013, Florian Haftmann wrote:

> Repair it or burn it?

I can't say anything specific -- Lukas Bulwahn has many more dead things 
still lying around.  The HOL/ROOT files contains various FIXME comments 
with dates attached.

At some point I need to make a tool like "isabelle sources" (as a reduced 
version of "isabelle build") with a few sanity checks over the directory 
structure to reveal disconnected parts.  It should probably also indicate 
raw unicode characters being left over from copy-paste accidents (or 
misunderstanding how Isabelle symbols work).


 	Makarius



More information about the isabelle-dev mailing list