PROGN$

execute a sequence of forms and return the value of the last one 
Major Section:  ACL2-BUILT-INS

This macro expands to a corresponding nest of calls of prog2$; see prog2$. The examples below show how this works: the first case below is typical, but we conclude with two special cases. 

ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x))
 (PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X)))
ACL2 !>:trans1 (progn$ (f1 x) (f2 x))
 (PROG2$ (F1 X) (F2 X))
ACL2 !>:trans1 (progn$ (f1 x))
 (F1 X)
ACL2 !>:trans1 (progn$)
 NIL
ACL2 !>