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 <nip...@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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
