[isabelle-dev] NEWS: toplevel theorem statements
makarius at sketis.net
Sun Oct 11 20:06:04 CEST 2015
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
> 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'.
More information about the isabelle-dev