[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.