Using defattach for execution of constrained functions
Nathan Wetzler
September 8, 2011

Defattach is a relatively new feature in ACL2 that allows the user to
extend the current theory with executability in a consistent manner.
In this talk, we will begin by discussing the use of encapsulate to
introduce constrained functions.  Next, we will introduce defattach
and look at its effect on the current theory.  We will then provide
some examples of defattach and give motivation for its use.  Finally,
we will examine a specific case of using defattach where the
constrained function bodies are the same as the executable function
bodies.