[isabelle-dev] Issues with unnamed top-level facts in Isabelle

Makarius makarius at sketis.net
Mon Nov 9 14:40:20 CET 2020

On 05/11/2020 17:04, Fabian Huch wrote:
> unused_thms reporting thms that are not unused does seem strange to me.

I will come back to this soon (presently diverging into other old mails).


More information about the isabelle-dev mailing list