[isabelle-dev] NEWS: antiquoted cartouches

Makarius makarius at sketis.net
Tue Dec 5 17:18:26 CET 2017

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

* Named control symbols (without special Unicode rendering) are shown as
bold-italic keyword. This is particularly useful for the short form of
antiquotations with control symbol: \<^name>\<open>argument\<close>. The
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
arguments into this format.

This refers to Isabelle/540eeaf88a63.

Still required: update of various ML antiquotations to allow cartouche
arguments. Right now it already works e.g. for @{typ}, @{term}, @{prop}.


More information about the isabelle-dev mailing list