I would like to use both 'min' operations in the prelude: min over a set and min of two values - how do I do it? In the former, I think the min found in 'min_nat' would do the trick, but I'm not sure how to access it. PVS always seems to think I want the min within 'real_defs' (which I do, for the latter). jerome