Tobias
On 05/11/2020 16:48, Makarius wrote:
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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
