[isabelle-dev] NEWS: toplevel theorem statements

Lawrence Paulson lp15 at cam.ac.uk
Sun Oct 11 11:32:31 CEST 2015

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. 


> 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

More information about the isabelle-dev mailing list