I'm thinking about the appropriate namespace for a recursion operator for wellfounded relations.<br>In HOL4 it is called WFREC and is in relationTheory.<br>In fact there is a small suite of related definitions there: RESTRICT, approx, and the_fun.<br>
I'm wondering if the list has any ideas about an appropriate way to package these things up (i.e. under what name, or with what other stuff).<br>I realize I may need to give more background about what they actually do... (don't have that on me at the moment!)<br>