Re: [isabelle] Trouble selecting maximum element of locally linear relation
On Thu, Mar 20, 2008 at 2:45 AM, Tobias Nipkow <nipkow at in.tum.de> 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