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). Makarius