*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LaTeX output for bounded Unions*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 15 Oct 2017 13:07:38 +0200*In-reply-to*: <VI1PR0301MB25251135F167EAE1A5B16E58B74B0@VI1PR0301MB2525.eurprd03.prod.outlook.com>*References*: <VI1PR0301MB25251135F167EAE1A5B16E58B74B0@VI1PR0301MB2525.eurprd03.prod.outlook.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.4.0

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**

**References**:**[isabelle] LaTeX output for bounded Unions***From:*Urban, Christian

- Previous by Date: [isabelle] Automating a Repetitive Structured Proof
- Next by Date: Re: [isabelle] List.nth_drop
- Previous by Thread: [isabelle] LaTeX output for bounded Unions
- Next by Thread: [isabelle] Isabelle functions: Always total, sometimes undefined
- Cl-isabelle-users October 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list