Re: [isabelle] extending well-founded partial orders to total well-founded orders
On 02/21/2013 07:22 PM, Andrei Popescu wrote:
Just to be clear: That's what I intended with my separate mail on
isabelle-dev (containing a polished theory file).
>> Find the (not yet polished) proofs attached
>> (I gather that calls to the smt method are nothing we want in
finished proofs, right?).
This matters only if you want to contribute the theorem as part of the
distribution. IMO, it is a useful theorem and it should be included.
My rational being that inclusion into the distribution is for developers
rather than users ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and