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

Christian



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