[isabelle] Fwd: Max of set in Isabelle

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.