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