print a string
Major Section:  IO

Use princ$ to print a string, without the surrounding double-quotes. Princ$ returns state.

ACL2 !>(princ$ "Howdy ho" (standard-co state) state)
Howdy ho<state>
ACL2 !>(pprogn (princ$ "Howdy ho" (standard-co state) state)
               (newline (standard-co state) state))
Howdy ho
ACL2 !>

See fmt for more sophisticated printing routines, and see IO for general information about input and output.