[isabelle] LaTeX output for bounded Unions

Dear All,

I have two small problems. I use the notation

   U i \<in> {..n} . P i     and   U i \<in> {n..m} . P i

for unions where the index is drawn from an interval. If

I print them out in LaTeX, the first is displayed as

  U i \<le> n . P i

I would prefer to have it uniformly displayed as interval, like

the  second. What do I have to do for that? I could not find

any syntax declaration which causes the first.

My second problem is that the theorems in question

seem to be printed eta-contracted like

  L(UPNTIMES r n) = UNION {..n} (SpecExt.Pow (L(r)))

even if I explicitly told Isabelle not to do it (set eta_contract = false).

How can I prevent this eta-contractions from happening?

Thanks a lot!


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