[isabelle-dev] NEWS: cartouches
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
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