Re: [isabelle] LaTeX output for bounded Unions

On 12/10/2017 15:46, Urban, Christian wrote:
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.

See Set_Interval, at the beginning.

I recommend not to use {..n::nat} because it means the same as {0..n}
but not all lemmas may exist for the former variant.

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?

Are you sure the internal term is really eta-expanded? If it comes
from a fun-definition, it is likely to get eta-contracted when you
make the definition. You may have to state an explicit eta-expanded


Thanks a lot!


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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