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

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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