Re: [isabelle-dev] NEWS: toplevel theorem statements

[Lawrence Paulson]

This suggestion was mine. Although “proposition” can mean many things, we are 
talking about mathematical developments. Quite a common convention is to 
reserve “theorem” for one or two main results, and “lemma” for technical 
results of no general interest, leaving “proposition” as the main vehicle for 
developing a theory. This will be especially important when people create 
papers directly from Isabelle theories. 

Larry

> On 11 Oct 2015, at 06:57, Tobias Nipkow  wrote:
> 
> 
> 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
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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



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