  ACL2 has long supported user-defined simplifiers, so-called metafunctions and
clause processors, which are installed when corresponding rules of class :meta
or :clause-processor are proved. Historically, such simplifiers could access
the logical world at execution time and could call certain built-in proof
tools, but one could not assume the soundness of the proof tools or the truth
of any facts extracted from the world or context when proving a simplifier
correct. Starting with ACL2 Version 6.0, released in December 2012, an
additional capability was added which allows the correctness proofs of
simplifiers to assume the correctness of some such proof tools and extracted
facts. In this paper we explain this capability and give examples that
demonstrate its utility.
