unused_thms reporting thms that are not unused does seem strange to me.
Fabian
On 05/11/2020 16:39, Fabian Huch wrote:
unnamed facts at the top level of a theory (i.e., unnamed lemmas or theorems)
don't work smoothly with the rest of Isabelle.
I see three possible ways to do improve this:
This behaviour it formal items with empty name binding is rather profound in
Isabelle.
The treatment of unnamed facts in particular is also fairly canonical
concerning our own standards.
Can you say what is wrong with this, and why it needs to be "improved"?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
