[isabelle] Document processing with XeLaTeX and unicode symbols



I have some text in my theory using quotation marks, e.g.:

text{* In the proof of the main theorem from the lecture notes, the
concept of a »fixed copy« of a graph is fundamental. *}

On disk, this is translated to:

text{* In the proof of the main theorem from the lecture notes, the
concept of a \<guillemotright>fixed copy\<guillemotleft> of a graph is
fundamental. *}

After running

$ isabelle usedir -b -D document Girth_Chromatic Ugraph_Properties

the TeX sources still contain the token '\<guillemotright>' and xelatex
complains about an undefined control sequence. (*)

Interestingly enough, such a translation doesn't happen for the symbols
'›' and '‹'.

Is there any way I could keep using '»' and '«' as quotation marks?


(*) side note: xelatex is able to process Unicode tokens, so it would be
fine if the .thy or .tex file simply contained '»' and '«'.






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