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