# Re: [isabelle] Partially terminating functions

`The confusion about partial termination in the function package could
``possibly be solved by modifying the theorem searcher.
`

`Abbreviations such as rec_fun_dom are easily confused for constants. The
``problem is that the theorem searcher doesn't help to distinguish them.
`

`When accidentally searching for abbreviations within your own theories it
``is usually clear that the theorem searcher is displaying less results
``than it should. Constants generated by automatic packages, however, are
``assumed to be special cases. It is easy to believe that few rules are
``available.
`

`Perhaps the theorem searcher could solve these problems by warning that
``one of the input terms is an abbreviation, and that more facts might be
``available for its constituent parts. I'm not sure how to implement
``this, but I think it would save some confusion.
`

`Another solution would be to have yet another colour scheme in Proof
``Genereal to help identify abbreviations. I suspect this might be overkill.
`
Yours,
Thomas.

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