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

Hi Christian, 

>> 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.   


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