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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev