Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)

\<^bsub> and \<^esub> cannot be part of the name of an identifier (variable, function, constant, ...), they are meant to be used for subscripting terms in mixfix syntax. If you want to have subscripts for identifiers, you must stick to \<^sub>. If the index consists of several letters, each must carry its own \<^sub> as in x\<^sub>1\<^sub>2. Conversely, when you define your own syntax for a function in which terms are subscripted, only use \<^bsub> and \<^esub>, but not \<^sub>. Otherwise, you will get strange effects.

Hope this helps,

On 18/02/15 21:35, W. Douglas Maurer wrote:
I normally just use \mathbb{Z} with the amssymb package loaded.

Thanks! This works! I wish it had been illustrated either in Lamport's LaTeX book or in
the LaTeX Companion.
The reason I'm full of such relatively low-level questions is that I live in the
Washington area (I'm retired from George Washington University) and I haven't been able to
find other people in the Washington area to talk to about Isabelle/Isar. Is there any
resource for this?
Right now I'm trying to use real subscripts, such as x-sub-1 where the 1 is set below the
line. This works (type x, push the \<^sub> button under Control in the Symbols pane, then
type 1) and x-sub-1, typed in this way, works as an identifier. Multi-character
subscripts, however, such as x-sub-12, have not been working. I'm supposed to type x, push
the \<^bsub> button under Control Block in the Symbols pane, type 12, then push the
\<^esub> button under Control Block) but that doesn't work for me, and the error message
I'm getting is saying that Isabelle isn't recognizing \<^bsub> at all. Am I doing this
right, or is there something else I have to do? Thanks! -WDMaurer
Prof. W. Douglas Maurer       Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University Fax  (1-202)994-4875

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