Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] cartouche-based antiquotation syntax for @{thm...

Email Gateway (Apr 22 2025 at 11:22):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Hi List,

during the last Isabelle versions, more and more syntax of the form
\<^name>\<open>arguments\<close> has been introduced as alias for the
standard antiquotation syntax @{name arguments}. We have,e.g.,

\<^typ>‹'a›
    \<^term>‹True›

but there's a notable exception: there's no such syntax for @{thm ...  }
and @{thms ...}. Is there any specific reason, or is this just an oversight?

--

Peter

Last updated: May 06 2025 at 08:28 UTC