Function Memoization and Unique Explicit Object Representation
		      Bob Boyer and Warren Hunt

We have created a version of ACL2 where every explicit object has a
single, unique internal representation.  For functions with domains
using only such uniquely represented arguments, we provide a function
memoization facility that stores values computed by memoized functions
so they may later be reused.

To enable our implementation of such uniquely representated objects,
we defined a function HONS, that has the semantics of CONS.  The
implementation of HONS ensures that whenever a call to HONS is made
with the same arguments of a previous call, the originally created
CONS pair is returned.  Such an implementation is satisfactory for
objects used and returned by ACL2 functions as ACL2 is used as a
functional programming language.

We define these facilities by giving their ACL2 definitions.  We also
describe some of the corresponding "under the hood" changes that were
made in the ACL2 system to enable these features.