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

Email Gateway (May 22 2025 at 13:47):

From: Makarius <makarius@sketis.net>
On 22/04/2025 13:22, Peter Lammich (via cl-isabelle-users Mailing List) wrote:

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?

The specific reason is that the argument syntax for @{thm ...} is more
flexible than just a single cartouche (as for @{typ} and @{term}), and that a
cartouche as a fact a different meaning (literal fact).

One happy day, I will revisit this and sort it all out.

For the meantime, note that the ML antiquotations \<^typ> and \<^term> are a
bit old-fashioned: \<^Type>, \<^Const> etc. or \<^instantiate> are better.

Makarius

Last updated: May 30 2025 at 04:27 UTC