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`;;