The documentation says that REWRITE_TAC;
"Rewrites a goal including built-in tautologies in the list of rewrites."
where SIMP_TAC ;
Rewrites a goal including built-in tautologies in the list of rewrites.
These look like they do the same thing to me but appear to have different effects.
Any ideas?