Basic infrastructure for using the HOL/TeX munger in place.