Re: [isabelle] feature request: defining tuples

On Thu, 28 Nov 2013, John Wickerson wrote:

Could I make a feature request regarding the "definition" package?

For me this is a genuine "feature", i.e. could be done or could be done differently. I've myself considered it around 1996, and rejected the idea as too much extra complication (after discussion with Konrad Slind and John Harrison).

We need to strive to *remove* more features that are not strictly necessary. All this is a heavy weight, and some day the system will just collapse due to the laws of gravity.


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