On 13/02/14 04:46, Vincent Aravantinos wrote:
Then considering leaving the goal unchanged, well it is a matter of taste... I
know it is the standard to leave the goal unchanged. But I personally met many
buggy situations that I hardly detected because HOL {4,Light} was just
allowing
a
Thanks, John! I'll read p 34 more carefully. Your example shows the behavior
I'd want from REWRITE_TAC. You theorem is
# ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
This is a good exercise for my right associativity skill. and that's what it
