[PVS-Help] Use of Common Lisp functions in ".el" file in batch mode

[Kyongho Min <min@xxxxxxxxxxxxxxx>]

Dear helpers,

Is there any way to use ACL common lisp functions in ".el" file in
batch mode? If I use some ACL functions inside (pvs-validate ... ) macro
block, then it returns undefined function error.

In my understanding, the el macro (pvs-validate ... ) in "pvs-utils.el" 
invokes PVS with ACL lisp (pvs-init) to prove a theory.

I wonder if it is possible to use ACL functions (e.g. parse-file, 
collect-tccs, found in "pvs.lisp") in "el" file in batch mode.

In addition, elisp functions solved my expectation with a little work.

Thanks a lot for your help.

regards,

min