Re: [isabelle] Another newbie proofs

Am Dienstag, den 12.03.2019, 16:46 +0000 schrieb Peter Lammich:
> The one [completion] on quotation marks was introduced to remember the
> user that cartouches should be used where possible, instead of quots.

This is the first time I hear that inner syntax parts can be enclosed by
cartouches instead of quotation marks. That also backquotes can be
replaced by cartouches was something I learned only after using Isabelle
for several months. Could the `prog-prove` tutorial be updated to
reflect these new conventions? I think this tutorial is the best
document to get into Isabelle and consequently should be up to date.

All the best,

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