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:



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