Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] antiquotation for a class

Email Gateway (Aug 22 2022 at 10:28):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gergely,

I use @{class pt} and expect that Isabelle would detail the definition
but it only prints

pt

in that respect @{class …} is similar to @{const …}.

Can I make Isabelle to print out the whole definition for a class?

You might consider writing your own antiquotation @{class_spec …}.

As of Isabelle2015, the following entrance points might be useful:

• ~~/src/Doc/antiquote_setup.ML for various examples how to define
  antiquotations

• Class.pretty_specification … for a slot providing a suitable
  representation

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 10:31):

From: Gergely Buday <gbuday@gmail.com>
Hi,

I use @{class pt} and expect that Isabelle would detail the definition
but it only prints

pt

Can I make Isabelle to print out the whole definition for a class?

• Gergely

Last updated: Apr 19 2024 at 12:27 UTC