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

Tobias



Thanks a lot!

Christian


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



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