Re: [isabelle] antiquotation for a class

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
* Class.pretty_specification â for a slot providing a suitable

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.