1; Like test1.lisp, but one big progn, and with a local event (which should be
2; skipped).
3
4(in-package "ACL2")
5
6(progn
7
8(defun foo (x)
9  (cons x x))
10
11(local (defun g (x) x))
12
13(defthm foo-prop
14  (equal (car (foo x))
15         x))
16
17(progn
18  (defun bar (x)
19    (foo x))
20  (defun h (x)
21    (bar x)))
22
23)
24