[isabelle-dev] NEWS: toplevel theorem statements

[Tobias Nipkow]

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.

Tobias

-------------- 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>