ACL2 Seminar, 5/10/06
MAKE-EVENT
Matt Kaufmann

Abstract.

I will talk about a new ACL2 feature, make-event, which will appear in the next
ACL2 release (and is available to play with, upon request).  It provides the
capability to do something like macro-expansion but with access to the ACL2
state and logical world.

My main goal in this talk is to give a sufficient preparation for users to
employ make-event in their work.  A secondary goal is to give a sense of what
was involved in implementing this feature.

Outline:

I.   Brief introduction to make-event from the documentation
II.  Some examples from books/make-event/*.lisp
III. More description of make-event, from the documentation
IV.  Brief introduction to semantics of make-event (:doc make-event-details)
V.   Some questions