[isabelle-dev] NEWS: cartouches

Makarius makarius at sketis.net
Tue May 24 20:24:56 CEST 2016

*** General ***

* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.

This refers e.g. to Isabelle/4cf6726eb85e, which also contains more
unification of "embedded" language tokens: type, term, prop, text. Thus
the complexity of Isabelle language nesting is reduced, thanks to more
uniform notation.

When demonstrating Isabelle occasionally to people who have never seen
it before, there is often a spontaneous puzzlement about ASCII quotes
around inner syntax. With cartouches that surprise might be avoided,
since it is not associated with already known syntax.

Still missing: a tool for systematic replacement of such semantic
cartouches. Purely syntactic ones are already handled by "isabelle


More information about the isabelle-dev mailing list