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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.