term_order : term -> term -> bool

SYNOPSIS
Term order for use in AC-rewriting.

DESCRIPTION
This binary predicate implements a crude but fairly efficient ordering on terms that is appropriate for ensuring that ordered rewriting will perform normalization.

FAILURE CONDITIONS
Never fails.

EXAMPLE
This example shows how using ordered rewriting with this term ordering can give normalization under associative and commutative laws given the appropriate rewrites:
  # ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p

\noindent
  # TOP_DEPTH_CONV
d + (f + a) + b + (c + e):num;;