Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] \<^locale> antiquotation does not work

view this post on Zulip Email Gateway (Aug 22 2022 at 18:03):

From: Peter Lammich <lammich@in.tum.de>
Hi

Although jedit offers me a shortcut and a template with a 
cartouche for \<^locale><...>, it does not work, while @{locale <...>}
works perfectly.

What is the correct/intended way to use \<^locale> ?

view this post on Zulip Email Gateway (Aug 22 2022 at 18:05):

From: Makarius <makarius@sketis.net>
E.g. as ML antiquotation.

The document antiquotations is still lagging behind in supporting
cartouche syntax, but it will be supported in the next release.

Makarius

Last updated: Apr 20 2024 at 04:19 UTC