[isabelle-dev] NEWS: toplevel theorem statements

[Makarius]

On Sun, 11 Oct 2015, Lawrence Paulson wrote:

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

When this request came up first on isabelle-users some weeks ago, I was 
about to answer like Tobias, also pointing to the existing 'prop' command.

Later I started looking through the sources, and came up with a 
simplification of the internal situation, and a reduction of the diversity 
of toplevel theorem statements.  So the total energy balance allowed to 
add this new alias of 'theorem'.


 	Makarius