I&#39;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&#39;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&#39;t have that on me at the moment!)<br>