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