[isabelle-dev] NEWS: toplevel theorem statements

Tobias Nipkow nipkow at in.tum.de
Sun Oct 11 07:57:33 CEST 2015

On 06/10/2015 21:46, Makarius wrote:
> * Toplevel theorem statement 'proposition' is another alias for
> 'theorem'.

Although this is consistent with the usage in mathematics, it is at odds with 
the usage in logic and in Isabelle where propositions are simply formulas, not 
necessarily provable ones.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151011/21be8098/attachment.bin>

More information about the isabelle-dev mailing list