[PVS-Help] opening files and batch mode

[Erika Rice <erice@cs.washington.edu>]

I want to use the batch mode of pvs and I want to open a file.  I run 
    pvs -batch -l file.el
where file.el contains
    (with-open-file (str "pvs-strategies-base" :direction :input)
      (do ((line (read-line str nil 'eof)
                 (read-line str nil 'eof)))
       ((eql line 'eof))
       (format t "~A~%" line)))

However, when I run this, I get an error saying with-open-file has a
void function definition.  

Why is this? Alternately, how can I read in a file for use in pvs
batch mode?

Thanks,

    Erika Rice