1all: 2 Holmake 3 cp ../../../examples/acl2/lisp/untranslate-file.lisp . 4 echo "(certify-book \"untranslate-file\")" | acl2 5 cat session1.lisp | acl2 6 cat session2.lisp | acl2 7 cat fact-out.lisp 8clean: 9 Holmake cleanAll 10 /bin/rm fact.lisp fact-out.* untranslate-file.* 11