[isabelle-dev] antiquotations and type_synonyms

Tobias Nipkow nipkow at in.tum.de
Thu Apr 18 17:47:33 CEST 2013

I was under the impression that type synonyms are expanded in typ
antiquotations, but apparently not, at least not with 30624dab6054. If I write
@{typ vname} I get "vname", even if vname is a type synonym for string. Maybe it
has always been like this, but it means that one cannot automatically display
(in latex) what some type synonym stands for, one has to type it in. Conversely,
if they were expanded, one could always prevent that with the [source] modifier.
Any views on this?


More information about the isabelle-dev mailing list