Polarity search functionality

[Eric-C-Hall]

Functionality that allows one to search for theorems such that a certain term specifically appears as a premise or as a conclusion to that theorem, rather than simply testing that the term is present somewhere in the theorem.

[mn200]

How about adjusting the Emacs code so that if the user provides a "prefix argument" (types C-u first), the sense of the search is flipped so that negative occurrences are searched for? See the elisp for hol-subgoal-tactic for how to do this:

• you add a parameter to the argument list p say
• you grab the value of the parameter with (interactive "P")
• the p will be non-nil if there has been a C-u typed.

[mn200]

BTW: your regression failures are a result of having used Unicode in files committed under src. There's an emacs command to fix this up semi-automatically. The rules allow the lambda and the magic quotes to be used even if everything else is forbidden.

[mn200]

Thanks for your work on this!