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

[Fabian Huch]

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