Sorry if I've missed your point (just a quick reply) but
On 01/06/2018 05:18 AM, Michael Beeson wrote:
SIMP isn't a conversion
SIMP_CONV is a conversion, which may give what you want
And if RHS_CONV would do what you want, no need to use PAT_CONV
Jeremy
Dear Michael,
On 05/01/2018 18:18, Michael Beeson wrote:
But, we have to rewrite ONLY that term, and not the other tarea terms.
We can do that kind of thing with PAT_CONV, but it only works on
conversions, and SIMP isn't a conversion, hence the convoluted code
above that makes REWRITE into a
Here is a fragment of working code (but depending on some previous stuff
not shown, so you can't just run this code). Since the code works, you
don't
need to run it--I'm just asking if it really needs to be this complicated.
Details below.
let tapermutation = MATCH_MP ta3 ta2;; # tarea(c,a,b)
Hello Michael,
I remember from my last time I used hol-light that the following code
from the flyspeck project was quite helpful:
(**
Add printers to HOL-Light to be able to print terms annotated with
their terms.
Snippet obtained from HOL-Light mailing list.