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.


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