DEFUN - define a function:
(defun f (x) (+ 1 x))

THM - prove an unnamed theorem:
(thm (equal (f (f x)) (+ 2 x)))

DEFTHM - prove a named theorem:
(defthm f-of-f (equal (f (f x)) (+ 2 x)))

IN-THEORY - change the list of currently enabled rules and functions
(in-theory (disable f))
(in-theory (enable f))

:U - undo an event
:u

:PBT - print history back through some numbered event
:pbt 1

:PE - print an event
:pe f-of-f

:PL - print rules matching a pattern
:pl (f (f x))

SET-GUARD-CHECKING - change whether ACL2 barfs on guard violations
:set-guard-checking nil

CERTIFY-BOOK - replay the proofs in a book and write certificate
(certify-book "script")

INCLUDE-BOOK - install events from a certified book into the current session
(include-book "script")

LD - load a file of events
(ld "script.lisp")



Some info on hints (more can be found here).  Hints always follow the keyword :hints, which follows
the formula to be proved inside the defthm, like this: 

(defthm ..name.. ..formula.. :hints ..hints..) 

Here, ..hints.. is a list of pairs, where each pair has a goal name and the
hints for that goal.  Here's a defthm with some hints (this doesn't make
much sense, I just wanted to use all the major kinds of hints):

(defthm app-of-cons
  (equal (app (cons x y) z)
         (cons x (app y z)))
  :hints (("Goal" 
           :in-theory (disable app)
           :induct (app x y)
           :expand (app x (app y z)))
          ("Subgoal *1/1"
           :use (:instance car-cons (x y))
           :do-not '(generalize eliminate-destructors))
          ("Subgoal *1/2"
           :cases ((integerp x) (consp x)))))



:IN-THEORY - change whether rules fire or functions open up (use enable or
disable)

:INDUCT - induct according to the induction scheme for the specified
function (app, above)

:EXPAND - expand the outmost function call in the specified term

:USE - use an instance of a lemma with the substitution specified

:DO-NOT - avoid things that seldom work, so that proofs fail faster

:CASES - consider each of the cases in the specified list, plus the case
in which all the specified cases fail to hold