Update from HH
[hl193./.git] / Tutorial / HOL_basics.ml
1 ARITH_RULE
2  `(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 +
3   (a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 =
4   (a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 +
5   (a * y + b * y + b * x) EXP 3 + (a * x) EXP 3`;;