 Kerber, Kohlhase &amp; Sorge 1998 use the Ωmega planning system as the overall way to integrate theorem proving and symbolic computation. In Harrison &amp; Théry 1998, we find an example of the integration of a higher-order logic theorem proving system (HOL) with a computer algebra system (Maple).