*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Inclusion-minimal sets*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 17 May 2016 10:14:51 +0200*In-reply-to*: <03b79e2f-5e0b-f9cd-9355-749f55ad0188@in.tum.de>*References*: <34e0baac-43b1-7d3f-a9ea-610ec59e69bb@in.tum.de> <6059DA05-CE9C-48E7-B7E9-1F7D7777A401@inria.fr> <0c7e8e69-6fdc-9456-4eb3-9894083cb452@in.tum.de> <03b79e2f-5e0b-f9cd-9355-749f55ad0188@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.0

I assume on weaker structures it would return some maximal element?

I have no objection in principle, but they way Max is defined would have to be reorganized considerably and you should talk to Florian about that.

I guess I'll put it on my queue then. Manuel

**References**:**[isabelle] Inclusion-minimal sets***From:*Manuel Eberl

**Re: [isabelle] Inclusion-minimal sets***From:*Jasmin Blanchette

**Re: [isabelle] Inclusion-minimal sets***From:*Manuel Eberl

**Re: [isabelle] Inclusion-minimal sets***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Inclusion-minimal sets
- Next by Date: Re: [isabelle] Lifting package and state transformers
- Previous by Thread: Re: [isabelle] Inclusion-minimal sets
- Next by Thread: [isabelle] Lifting package and state transformers
- Cl-isabelle-users May 2016 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