Re: [isabelle-dev] NEWS: toplevel theorem statements

2015-10-11 Thread Lawrence Paulson
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

Re: [isabelle-dev] NEWS: toplevel theorem statements

2015-10-10 Thread Tobias Nipkow
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