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