[isabelle-dev] src/Doc/Corec fails

[Makarius]

On Sat, 2 Apr 2016, Jasmin Blanchette wrote:

>> This works as long as only Isabelle antiquotations or control symbols 
>> are used.
>
> I don't know any good way of putting Isabelle text as produced by 
> antiquotations in bold. Do you?

How about this?

text ‹
   \def\isactrlbold#1{{\bfseries\itshape\boldmath#1}}

   ‹f.❙c❙o❙n❙g❙_❙C⇩1›
›


The subscript is not bold, but that is probably better mathematical 
typesetting anyway.


 	Makarius