Re: [isabelle] backslashes in constant names



On Tue, 2 Aug 2005, Stephan Merz wrote:

> constdefs
>   "\in"  :: "['a, 'a set] => bool"     (infixl 50)
>   "a \in S == a:S"

You certainly need to escape backslashes in the sources.


> and the PDF document shows the constant name as ``in.

It works for the default "tt" style; for "it" try this:

\renewcommand{\isacharbackslash}{\isamath{\backslash}}


	Makarius





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