To compile CASLtoPVS:

In linux:

export CLASSPATH=/home/dts/www/cofi/CASLtoPVS/aterm-0.18/java1.2/:/home/dts/www/cofi/CASLtoPVS:$CLASSPATH
setup jdk1.2
javac CASLtoPVS.java


To prove a theorem in PVS:

First typecheck all the adt files using M-x tcp, then typecheck the
main file using M-x tcp, then position the cursor on a theorem,
M-x pr, then type commands to do the proof, e.g. (grind)