Re: [isabelle] Fwd: Max of set in Isabelle

There is the prefined Max function in theory Big_Operators (which is part of
Main). It works for any linear order.


Am 20/01/2013 07:05, schrieb Konstantin Weitz:
> How can I find the maximum element in a set of numbers (nat) in Isabelle.
> The max function doesn't work, as it is only defined to take the maximum of
> two elements. I have an idea of how I could implement it using a reduce
> like function, but I don't know how to pick one random element from a set.

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