Re: [isabelle] Trouble selecting maximum element of locally linear relation

On Thu, Mar 20, 2008 at 2:45 AM, Tobias Nipkow <nipkow at> wrote:
> I don't think there is anything readymade anywhere. All I can suggest is
>  to take the development of Max in FiniteSet and generalize and adapt it
>  to your situation. The structure of the development should stay the
>  same, but of course many details will change.

Thank you all for your help.  In the end I used the proof developed by
Stefan which I believe is essentially what Tobias suggested.

Stefan, reading your proof was insightful and helpful.  Thanks again!


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