OK, my original example now works.
But I get exception Unchanged raised when I try IMP_REWRITE_TAC[] on the
goal ``p \/ q == q \/ p``.
I still would expect the tactic to be able to solve this goal, no?
And if it can't then would it not be better to leave the goal unchanged
rather than to raise an
I have a question about REWRITE_TAC. I was invited to speak at the conference
https://ihp2014.pps.univ-paris-diderot.fr/doku.php?id=workshop_1
where John, Freek, Tobias Nipkow and Tom Hales are 4 of the 14 plenary
speakers, and I hope folks here will help answer various HOL Light questions I
Here's a question about free variables and REWRITE_TAC (and other
thmlist-tactics). Almost every usage of USE_THEN in the HOL Light sources is
of the form
USE_THEN label MATCH_MP_TAC
Here's an example of a labeled assumption used in thmlist of MESON_TAC:
let NSQRT_2 = prove
(`!p q. p * p =
Hi Bill,
| I'm quite mystified that the REWRITE_TAC[DIST_SYM] only rewrote the
| middle dist term
Generally speaking, with constructs like REWRITE_TAC that apply
rewrites repeatedly, there are special heuristics to deal with those
that would obviously loop indefinitely. (This doesn't apply to
Hi Ramana,
this is intended: what makes the tactic solve p /\ q == q /\ p is
that it uses the context p /\ q when doing the rewriting. Therefore
the theorems used for the rewrite are p = T and q = T, which indeed
turns p /\ q into T /\ T.
However with p \/ q the context only brings (p \/
