[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 <nipkow at in.tum.de> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev