Re: [isabelle] making use of star
On Fri, 22 Jun 2012, James Smith wrote:
As an interesting aside, working with Isabelle in a room full of Coq
users seems to be working out fine. Those around me get an introduction
to basic Isabelle syntax amongst other things and I get valuable
conversations about theorem proving and types in general.
Exchange of Isabelle and Coq users can indeed be quite interesting to
learn more about the specifc strengths and weaknesses of either system,
although there is a substantial overlap.
BTW, when a Coq user says "type" he means "proposition" in a more common
sense, which is also the way Isabelle uses term. So
theorem a: A <proof>
is just a theorem called "a" with proposition "A", which is proven by the
included proof. A Coq user would call "a" constant and "A" type here.
Anyway, Isabelle also has some terminology that first needs some
interpretation to be understandable to other people out there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and