Re: [isabelle] extending well-founded partial orders to total well-founded orders



Hi Andrei,

On 02/21/2013 07:22 PM, Andrei Popescu wrote:
Hi Christian,

 >> Find the (not yet polished) proofs attached

Nice!

 >> (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.
Just to be clear: That's what I intended with my separate mail on isabelle-dev (containing a polished theory file).


http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/3865/match=

My rational being that inclusion into the distribution is for developers rather than users ;)

cheers

chris







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