# [isabelle] typesetting compound subscripts

Dear Isabelle,
How is it possible to introduce typeset syntax with compound
subscripts? For example, given an indexed family "tos" of relations,
where I currently write
(t1,t2) \<in> tos n
I'd like to write something that will be typeset roughly as the LaTeX
t1 \leq_{tos n} t2
(Here tos is a bound variable, not something introduced by a consts, if that makes any difference.)
My attempts have all failed miserably (except when the subscript is a
single-character identifier), trying various combinations of Isabelle
syntax and translations declarations, definitions of \isactrlfoo's,
and \<^bsub>...\<^esub>.
many thanks,
Peter
example:
types t = "string"
types indexed_orders = "nat \<Rightarrow> (t*t) set"
constdefs
mytest :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool"
"mytest tos n t1 t2 == (t1,t2) \<in> tos n"

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