Hi, I am using the Isar token translation mechanism to modify the latex generation of Isabelle.
token_translation {*
.....
*}
This works fine if if output stuff for example like that
text{*
@{thm float_add}
*}
But it does not work for the main output of a theory, like
lemma "balabla"
sorry
The token translations are not applied to "balabla". How can I fix this ?
Steven
