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



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.   

Andrei 






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