Update pvs to 3.2:

According to http://pvs.csl.sri.com/announcements/pvs3.2-release-notes.shtml
this contains a number of bug fixes as well as the following improvements
and added features:
-Startup Script Update
-Theory Interpretation Enhancements
-References to Mapped Entities
-Cleaning up Specifications
-Binary Files
-Generating HTML
-Default Strategies
-Better handling of TCCs in Proofs
-typepred! rule and all-typepreds strategy
-grind-with-ext and reduce-with-ext
-New forward chain commands
-TeX Substitutions
-add-declaration and IMPORTINGs
-Prelude additions

6 files changed, 122 insertions, 232 deletions

diff --git a/devel/pvs/Makefile b/devel/pvs/Makefile
index c02bc65a516..32945c45021 100644
--- a/devel/pvs/Makefile
+++ b/devel/pvs/Makefile
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.19 2005/08/28 04:25:29 uebayasi Exp $
+# $NetBSD: Makefile,v 1.20 2005/09/02 02:27:11 jschauma Exp $
 #
 
 DISTNAME=		pvs-${VERSION}
 PKGNAME=		${EMACS_PKGNAME_PREFIX}${DISTNAME}
-PKGREVISION=		2
 CATEGORIES=		devel lang
 MASTER_SITES=		ftp://pvs.csl.sri.com/pub/pvs/pvs${VERSION}/ \
 			ftp://ftp.cs.york.ac.uk/pub/pvs/pvs${VERSION}/ \
@@ -11,7 +10,6 @@ MASTER_SITES=		ftp://pvs.csl.sri.com/pub/pvs/pvs${VERSION}/ \
 EXTRACT_SUFX=		.tgz
 DISTFILES=		${DISTNAME}-${MAINFILEEXT}${EXTRACT_SUFX} \
 			pvs-${VERSION}-system${EXTRACT_SUFX} \
-			pvs-${VERSION}-emacs19${EXTRACT_SUFX} \
 			pvs-${VERSION}-libraries${EXTRACT_SUFX}
 
 MAINTAINER=		jschauma@NetBSD.org
@@ -22,7 +20,7 @@ DEPENDS+=		teTeX>=1.0.7:../../print/teTeX
 DEPENDS+=		tk>=8.0:../../x11/tk
 
 WRKSRC=			${WRKDIR}
-VERSION=		3.1
+VERSION=		3.2
 NO_BUILD=		# defined
 CHECK_SHLIBS=		NO
 SHLIB_HANDLING=		NO
diff --git a/devel/pvs/PLIST b/devel/pvs/PLIST
index 8cd6e581507..d73fe80208f 100644
--- a/devel/pvs/PLIST
+++ b/devel/pvs/PLIST
@@ -1,18 +1,8 @@
-@comment $NetBSD: PLIST,v 1.5 2004/02/16 16:55:43 seb Exp $
+@comment $NetBSD: PLIST,v 1.6 2005/09/02 02:27:11 jschauma Exp $
 bin/pvs
-pvs/Examples/README
-pvs/Examples/ackerman.pvs
-pvs/Examples/f91.pvs
-pvs/Examples/groups.pvs
-pvs/Examples/stack.pvs
-pvs/Examples/stacks.pvs
-pvs/Examples/sum.pvs
-pvs/Examples/sum2.pvs
-pvs/Examples/ustacks.pvs
 pvs/README
 pvs/bin/ix86-redhat5/runtime/file_utils.so
 pvs/bin/ix86-redhat5/runtime/files.bu
-pvs/bin/ix86-redhat5/runtime/ics_lisp.so
 pvs/bin/ix86-redhat5/runtime/libacl623.so
 pvs/bin/ix86-redhat5/runtime/mu.so
 pvs/bin/ix86-redhat5/runtime/pvs-allegro6.2
@@ -93,118 +83,6 @@ pvs/emacs/emacs-src/pvs-utils.el
 pvs/emacs/emacs-src/pvs-view.el
 pvs/emacs/emacs-src/pvs.xpm
 pvs/emacs/emacs-src/tcl.el
-pvs/emacs/emacs19/Makefile
-pvs/emacs/emacs19/comint-ipc.el
-pvs/emacs/emacs19/comint-ipc.elc
-pvs/emacs/emacs19/completer.el
-pvs/emacs/emacs19/completer.elc
-pvs/emacs/emacs19/completer.new.el
-pvs/emacs/emacs19/completer.no-fun.el
-pvs/emacs/emacs19/ilcompat.el
-pvs/emacs/emacs19/ilfsf18.el
-pvs/emacs/emacs19/ilfsf19.el
-pvs/emacs/emacs19/ilfsf20.el
-pvs/emacs/emacs19/ilisp-acl.el
-pvs/emacs/emacs19/ilisp-acl.elc
-pvs/emacs/emacs19/ilisp-aut.el
-pvs/emacs/emacs19/ilisp-aut.elc
-pvs/emacs/emacs19/ilisp-bat.el
-pvs/emacs/emacs19/ilisp-chs.el
-pvs/emacs/emacs19/ilisp-cl.el
-pvs/emacs/emacs19/ilisp-cl.elc
-pvs/emacs/emacs19/ilisp-cmp.el
-pvs/emacs/emacs19/ilisp-cmp.elc
-pvs/emacs/emacs19/ilisp-cmt.el
-pvs/emacs/emacs19/ilisp-cmt.elc
-pvs/emacs/emacs19/ilisp-def.el
-pvs/emacs/emacs19/ilisp-def.elc
-pvs/emacs/emacs19/ilisp-dia.el
-pvs/emacs/emacs19/ilisp-dia.elc
-pvs/emacs/emacs19/ilisp-doc.el
-pvs/emacs/emacs19/ilisp-doc.elc
-pvs/emacs/emacs19/ilisp-el.el
-pvs/emacs/emacs19/ilisp-el.elc
-pvs/emacs/emacs19/ilisp-ext.el
-pvs/emacs/emacs19/ilisp-ext.elc
-pvs/emacs/emacs19/ilisp-hi.el
-pvs/emacs/emacs19/ilisp-hi.elc
-pvs/emacs/emacs19/ilisp-hnd.el
-pvs/emacs/emacs19/ilisp-hnd.elc
-pvs/emacs/emacs19/ilisp-ind.el
-pvs/emacs/emacs19/ilisp-ind.elc
-pvs/emacs/emacs19/ilisp-inp.el
-pvs/emacs/emacs19/ilisp-inp.elc
-pvs/emacs/emacs19/ilisp-key.el
-pvs/emacs/emacs19/ilisp-key.elc
-pvs/emacs/emacs19/ilisp-kil.el
-pvs/emacs/emacs19/ilisp-kil.elc
-pvs/emacs/emacs19/ilisp-low.el
-pvs/emacs/emacs19/ilisp-low.elc
-pvs/emacs/emacs19/ilisp-menu.el
-pvs/emacs/emacs19/ilisp-mnb.el
-pvs/emacs/emacs19/ilisp-mod.el
-pvs/emacs/emacs19/ilisp-mod.elc
-pvs/emacs/emacs19/ilisp-mov.el
-pvs/emacs/emacs19/ilisp-mov.elc
-pvs/emacs/emacs19/ilisp-out.el
-pvs/emacs/emacs19/ilisp-out.elc
-pvs/emacs/emacs19/ilisp-prc.el
-pvs/emacs/emacs19/ilisp-prc.elc
-pvs/emacs/emacs19/ilisp-prn.el
-pvs/emacs/emacs19/ilisp-prn.elc
-pvs/emacs/emacs19/ilisp-rng.el
-pvs/emacs/emacs19/ilisp-rng.elc
-pvs/emacs/emacs19/ilisp-snd.el
-pvs/emacs/emacs19/ilisp-snd.elc
-pvs/emacs/emacs19/ilisp-src.el
-pvs/emacs/emacs19/ilisp-sym.el
-pvs/emacs/emacs19/ilisp-sym.elc
-pvs/emacs/emacs19/ilisp-utl.el
-pvs/emacs/emacs19/ilisp-utl.elc
-pvs/emacs/emacs19/ilisp-val.el
-pvs/emacs/emacs19/ilisp-val.elc
-pvs/emacs/emacs19/ilisp-xfr.el
-pvs/emacs/emacs19/ilisp-xfr.elc
-pvs/emacs/emacs19/ilisp-xls.el
-pvs/emacs/emacs19/ilisp.el
-pvs/emacs/emacs19/illuc19.el
-pvs/emacs/emacs19/ilxemacs.el
-pvs/emacs/emacs19/pvs-abbreviations.el
-pvs/emacs/emacs19/pvs-abbreviations.elc
-pvs/emacs/emacs19/pvs-browser.el
-pvs/emacs/emacs19/pvs-browser.elc
-pvs/emacs/emacs19/pvs-byte-compile.el
-pvs/emacs/emacs19/pvs-cmds.el
-pvs/emacs/emacs19/pvs-cmds.elc
-pvs/emacs/emacs19/pvs-eval.el
-pvs/emacs/emacs19/pvs-eval.elc
-pvs/emacs/emacs19/pvs-file-list.el
-pvs/emacs/emacs19/pvs-file-list.elc
-pvs/emacs/emacs19/pvs-ilisp.el
-pvs/emacs/emacs19/pvs-load.el
-pvs/emacs/emacs19/pvs-load.elc
-pvs/emacs/emacs19/pvs-macros.el
-pvs/emacs/emacs19/pvs-macros.elc
-pvs/emacs/emacs19/pvs-menu.el
-pvs/emacs/emacs19/pvs-menu.elc
-pvs/emacs/emacs19/pvs-mode.el
-pvs/emacs/emacs19/pvs-mode.elc
-pvs/emacs/emacs19/pvs-prelude-files-and-regions.el
-pvs/emacs/emacs19/pvs-print.el
-pvs/emacs/emacs19/pvs-print.elc
-pvs/emacs/emacs19/pvs-prover-helps.el
-pvs/emacs/emacs19/pvs-prover-helps.elc
-pvs/emacs/emacs19/pvs-prover.el
-pvs/emacs/emacs19/pvs-prover.elc
-pvs/emacs/emacs19/pvs-set-prelude-info.el
-pvs/emacs/emacs19/pvs-tcl.el
-pvs/emacs/emacs19/pvs-tcl.elc
-pvs/emacs/emacs19/pvs-utils.el
-pvs/emacs/emacs19/pvs-utils.elc
-pvs/emacs/emacs19/pvs-view.el
-pvs/emacs/emacs19/pvs-view.elc
-pvs/emacs/emacs19/tcl.el
-pvs/emacs/emacs19/tcl.elc
 pvs/emacs/emacs20/comint-ipc.el
 pvs/emacs/emacs20/comint-ipc.elc
 pvs/emacs/emacs20/completer.el
@@ -292,6 +170,7 @@ pvs/emacs/emacs20/pvs-eval.elc
 pvs/emacs/emacs20/pvs-file-list.el
 pvs/emacs/emacs20/pvs-file-list.elc
 pvs/emacs/emacs20/pvs-ilisp.el
+pvs/emacs/emacs20/pvs-ilisp.elc
 pvs/emacs/emacs20/pvs-load.el
 pvs/emacs/emacs20/pvs-load.elc
 pvs/emacs/emacs20/pvs-macros.el
@@ -404,6 +283,7 @@ pvs/emacs/xemacs21/pvs-eval.elc
 pvs/emacs/xemacs21/pvs-file-list.el
 pvs/emacs/xemacs21/pvs-file-list.elc
 pvs/emacs/xemacs21/pvs-ilisp.el
+pvs/emacs/xemacs21/pvs-ilisp.elc
 pvs/emacs/xemacs21/pvs-load.el
 pvs/emacs/xemacs21/pvs-load.elc
 pvs/emacs/xemacs21/pvs-macros.el
@@ -428,203 +308,219 @@ pvs/emacs/xemacs21/pvs-view.el
 pvs/emacs/xemacs21/pvs-view.elc
 pvs/emacs/xemacs21/tcl.el
 pvs/emacs/xemacs21/tcl.elc
+pvs/lib/bitvectors/.cvsignore
 pvs/lib/bitvectors/.pvscontext
-pvs/lib/bitvectors/BitvectorMultiplication.bin
 pvs/lib/bitvectors/BitvectorMultiplication.prf
 pvs/lib/bitvectors/BitvectorMultiplication.pvs
-pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.bin
 pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.prf
 pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.pvs
-pvs/lib/bitvectors/BitvectorOneComplementDivision.bin
 pvs/lib/bitvectors/BitvectorOneComplementDivision.prf
 pvs/lib/bitvectors/BitvectorOneComplementDivision.pvs
-pvs/lib/bitvectors/BitvectorTwoComplementDivision.bin
 pvs/lib/bitvectors/BitvectorTwoComplementDivision.prf
 pvs/lib/bitvectors/BitvectorTwoComplementDivision.pvs
-pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.bin
 pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.prf
+pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.prf.bak
 pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.pvs
-pvs/lib/bitvectors/BitvectorUtil.bin
 pvs/lib/bitvectors/BitvectorUtil.prf
+pvs/lib/bitvectors/BitvectorUtil.prf.bak
 pvs/lib/bitvectors/BitvectorUtil.pvs
-pvs/lib/bitvectors/DivisionUtil.bin
+pvs/lib/bitvectors/BitvectorUtil.pvs.bak
 pvs/lib/bitvectors/DivisionUtil.prf
 pvs/lib/bitvectors/DivisionUtil.pvs
-pvs/lib/bitvectors/bv_adder.bin
 pvs/lib/bitvectors/bv_adder.prf
 pvs/lib/bitvectors/bv_adder.pvs
-pvs/lib/bitvectors/bv_arith_caret.bin
 pvs/lib/bitvectors/bv_arith_caret.prf
 pvs/lib/bitvectors/bv_arith_caret.pvs
-pvs/lib/bitvectors/bv_arith_caret_concat_rules.bin
 pvs/lib/bitvectors/bv_arith_caret_concat_rules.prf
 pvs/lib/bitvectors/bv_arith_caret_concat_rules.pvs
-pvs/lib/bitvectors/bv_arith_caret_rules.bin
 pvs/lib/bitvectors/bv_arith_caret_rules.prf
 pvs/lib/bitvectors/bv_arith_caret_rules.pvs
-pvs/lib/bitvectors/bv_arith_concat.bin
 pvs/lib/bitvectors/bv_arith_concat.prf
 pvs/lib/bitvectors/bv_arith_concat.pvs
-pvs/lib/bitvectors/bv_arith_extend.bin
 pvs/lib/bitvectors/bv_arith_extend.prf
 pvs/lib/bitvectors/bv_arith_extend.pvs
-pvs/lib/bitvectors/bv_arith_int_caret.bin
 pvs/lib/bitvectors/bv_arith_int_caret.prf
 pvs/lib/bitvectors/bv_arith_int_caret.pvs
-pvs/lib/bitvectors/bv_arith_int_concat.bin
 pvs/lib/bitvectors/bv_arith_int_concat.prf
 pvs/lib/bitvectors/bv_arith_int_concat.pvs
-pvs/lib/bitvectors/bv_arith_int_rules.bin
 pvs/lib/bitvectors/bv_arith_int_rules.prf
 pvs/lib/bitvectors/bv_arith_int_rules.pvs
-pvs/lib/bitvectors/bv_arith_minus_rules.bin
 pvs/lib/bitvectors/bv_arith_minus_rules.prf
 pvs/lib/bitvectors/bv_arith_minus_rules.pvs
-pvs/lib/bitvectors/bv_arith_nat.bin
 pvs/lib/bitvectors/bv_arith_nat.prf
 pvs/lib/bitvectors/bv_arith_nat.pvs
-pvs/lib/bitvectors/bv_arith_nat_caret_rules.bin
 pvs/lib/bitvectors/bv_arith_nat_caret_rules.prf
 pvs/lib/bitvectors/bv_arith_nat_caret_rules.pvs
-pvs/lib/bitvectors/bv_arith_nat_rules.bin
 pvs/lib/bitvectors/bv_arith_nat_rules.prf
 pvs/lib/bitvectors/bv_arith_nat_rules.pvs
-pvs/lib/bitvectors/bv_arith_rules.bin
 pvs/lib/bitvectors/bv_arith_rules.prf
 pvs/lib/bitvectors/bv_arith_rules.pvs
-pvs/lib/bitvectors/bv_arithmetic.bin
 pvs/lib/bitvectors/bv_arithmetic.prf
 pvs/lib/bitvectors/bv_arithmetic.pvs
-pvs/lib/bitvectors/bv_bitwise_rules.bin
 pvs/lib/bitvectors/bv_bitwise_rules.prf
 pvs/lib/bitvectors/bv_bitwise_rules.pvs
-pvs/lib/bitvectors/bv_caret_bitwise.bin
 pvs/lib/bitvectors/bv_caret_bitwise.prf
 pvs/lib/bitvectors/bv_caret_bitwise.pvs
-pvs/lib/bitvectors/bv_caret_bitwise_rules.bin
 pvs/lib/bitvectors/bv_caret_bitwise_rules.prf
 pvs/lib/bitvectors/bv_caret_bitwise_rules.pvs
-pvs/lib/bitvectors/bv_caret_concat.bin
 pvs/lib/bitvectors/bv_caret_concat.prf
 pvs/lib/bitvectors/bv_caret_concat.pvs
-pvs/lib/bitvectors/bv_caret_concat_rules.bin
 pvs/lib/bitvectors/bv_caret_concat_rules.prf
 pvs/lib/bitvectors/bv_caret_concat_rules.pvs
-pvs/lib/bitvectors/bv_caret_rules.bin
 pvs/lib/bitvectors/bv_caret_rules.prf
 pvs/lib/bitvectors/bv_caret_rules.pvs
-pvs/lib/bitvectors/bv_concat.bin
 pvs/lib/bitvectors/bv_concat.prf
 pvs/lib/bitvectors/bv_concat.pvs
-pvs/lib/bitvectors/bv_concat_rules.bin
 pvs/lib/bitvectors/bv_concat_rules.prf
 pvs/lib/bitvectors/bv_concat_rules.pvs
-pvs/lib/bitvectors/bv_constants.bin
 pvs/lib/bitvectors/bv_constants.prf
 pvs/lib/bitvectors/bv_constants.pvs
-pvs/lib/bitvectors/bv_core.bin
 pvs/lib/bitvectors/bv_core.pvs
-pvs/lib/bitvectors/bv_extend.bin
 pvs/lib/bitvectors/bv_extend.prf
 pvs/lib/bitvectors/bv_extend.pvs
-pvs/lib/bitvectors/bv_fract.bin
 pvs/lib/bitvectors/bv_fract.prf
 pvs/lib/bitvectors/bv_fract.pvs
-pvs/lib/bitvectors/bv_int.bin
 pvs/lib/bitvectors/bv_int.prf
 pvs/lib/bitvectors/bv_int.pvs
-pvs/lib/bitvectors/bv_mult_div_rem.bin
 pvs/lib/bitvectors/bv_mult_div_rem.prf
 pvs/lib/bitvectors/bv_mult_div_rem.pvs
-pvs/lib/bitvectors/bv_nat_rules.bin
 pvs/lib/bitvectors/bv_nat_rules.prf
 pvs/lib/bitvectors/bv_nat_rules.pvs
-pvs/lib/bitvectors/bv_notes.bin
 pvs/lib/bitvectors/bv_notes.pvs
-pvs/lib/bitvectors/bv_overflow.bin
 pvs/lib/bitvectors/bv_overflow.prf
 pvs/lib/bitvectors/bv_overflow.pvs
-pvs/lib/bitvectors/bv_rotate.bin
 pvs/lib/bitvectors/bv_rotate.prf
 pvs/lib/bitvectors/bv_rotate.pvs
-pvs/lib/bitvectors/bv_rules.bin
 pvs/lib/bitvectors/bv_rules.pvs
-pvs/lib/bitvectors/bv_shift.bin
 pvs/lib/bitvectors/bv_shift.prf
 pvs/lib/bitvectors/bv_shift.pvs
-pvs/lib/bitvectors/bv_sum.bin
 pvs/lib/bitvectors/bv_sum.prf
 pvs/lib/bitvectors/bv_sum.pvs
-pvs/lib/bitvectors/div.bin
 pvs/lib/bitvectors/div.prf
 pvs/lib/bitvectors/div.pvs
-pvs/lib/bitvectors/floor_div_props.bin
 pvs/lib/bitvectors/floor_div_props.prf
 pvs/lib/bitvectors/floor_div_props.pvs
-pvs/lib/bitvectors/mod.bin
 pvs/lib/bitvectors/mod.prf
+pvs/lib/bitvectors/mod.prf.bak
 pvs/lib/bitvectors/mod.pvs
-pvs/lib/bitvectors/mod_rules.bin
 pvs/lib/bitvectors/mod_rules.prf
 pvs/lib/bitvectors/mod_rules.pvs
-pvs/lib/bitvectors/orphaned-proofs.prf
-pvs/lib/bitvectors/sums.bin
+pvs/lib/bitvectors/pvsbin/BitvectorMultiplication.bin
+pvs/lib/bitvectors/pvsbin/BitvectorMultiplicationWidenNarrow.bin
+pvs/lib/bitvectors/pvsbin/BitvectorOneComplementDivision.bin
+pvs/lib/bitvectors/pvsbin/BitvectorTwoComplementDivision.bin
+pvs/lib/bitvectors/pvsbin/BitvectorTwoComplementDivisionWidenNarrow.bin
+pvs/lib/bitvectors/pvsbin/BitvectorUtil.bin
+pvs/lib/bitvectors/pvsbin/DivisionUtil.bin
+pvs/lib/bitvectors/pvsbin/bv_adder.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_caret.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_caret_concat_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_caret_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_concat.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_extend.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_int_caret.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_int_concat.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_int_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_minus_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_nat.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_nat_caret_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_nat_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arith_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_arithmetic.bin
+pvs/lib/bitvectors/pvsbin/bv_bitwise_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_caret_bitwise.bin
+pvs/lib/bitvectors/pvsbin/bv_caret_bitwise_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_caret_concat.bin
+pvs/lib/bitvectors/pvsbin/bv_caret_concat_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_caret_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_concat.bin
+pvs/lib/bitvectors/pvsbin/bv_concat_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_constants.bin
+pvs/lib/bitvectors/pvsbin/bv_core.bin
+pvs/lib/bitvectors/pvsbin/bv_extend.bin
+pvs/lib/bitvectors/pvsbin/bv_fract.bin
+pvs/lib/bitvectors/pvsbin/bv_int.bin
+pvs/lib/bitvectors/pvsbin/bv_mult_div_rem.bin
+pvs/lib/bitvectors/pvsbin/bv_nat_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_notes.bin
+pvs/lib/bitvectors/pvsbin/bv_overflow.bin
+pvs/lib/bitvectors/pvsbin/bv_rotate.bin
+pvs/lib/bitvectors/pvsbin/bv_rules.bin
+pvs/lib/bitvectors/pvsbin/bv_shift.bin
+pvs/lib/bitvectors/pvsbin/bv_sum.bin
+pvs/lib/bitvectors/pvsbin/div.bin
+pvs/lib/bitvectors/pvsbin/floor_div_props.bin
+pvs/lib/bitvectors/pvsbin/mod.bin
+pvs/lib/bitvectors/pvsbin/mod_rules.bin
+pvs/lib/bitvectors/pvsbin/sums.bin
+pvs/lib/bitvectors/pvsbin/top.bin
 pvs/lib/bitvectors/sums.prf
 pvs/lib/bitvectors/sums.pvs
-pvs/lib/bitvectors/top.bin
 pvs/lib/bitvectors/top.pvs
 pvs/lib/character_adt.pvs
+pvs/lib/finite_sets/.cvsignore
 pvs/lib/finite_sets/.pvscontext
-pvs/lib/finite_sets/finite_sets_below.bin
+pvs/lib/finite_sets/finite_cross.prf
+pvs/lib/finite_sets/finite_cross.pvs
 pvs/lib/finite_sets/finite_sets_below.prf
 pvs/lib/finite_sets/finite_sets_below.pvs
-pvs/lib/finite_sets/finite_sets_card_eq.bin
 pvs/lib/finite_sets/finite_sets_card_eq.prf
 pvs/lib/finite_sets/finite_sets_card_eq.pvs
-pvs/lib/finite_sets/finite_sets_eq.bin
 pvs/lib/finite_sets/finite_sets_eq.prf
 pvs/lib/finite_sets/finite_sets_eq.pvs
-pvs/lib/finite_sets/finite_sets_inductions.bin
 pvs/lib/finite_sets/finite_sets_inductions.prf
 pvs/lib/finite_sets/finite_sets_inductions.pvs
-pvs/lib/finite_sets/finite_sets_int.bin
 pvs/lib/finite_sets/finite_sets_int.prf
+pvs/lib/finite_sets/finite_sets_int.prf.bak
 pvs/lib/finite_sets/finite_sets_int.pvs
-pvs/lib/finite_sets/finite_sets_minmax.bin
 pvs/lib/finite_sets/finite_sets_minmax.prf
 pvs/lib/finite_sets/finite_sets_minmax.pvs
-pvs/lib/finite_sets/finite_sets_nat.bin
+pvs/lib/finite_sets/finite_sets_minmax_props.prf
+pvs/lib/finite_sets/finite_sets_minmax_props.pvs
 pvs/lib/finite_sets/finite_sets_nat.prf
 pvs/lib/finite_sets/finite_sets_nat.pvs
-pvs/lib/finite_sets/finite_sets_pred.bin
 pvs/lib/finite_sets/finite_sets_pred.prf
 pvs/lib/finite_sets/finite_sets_pred.pvs
-pvs/lib/finite_sets/finite_sets_sum.bin
 pvs/lib/finite_sets/finite_sets_sum.prf
 pvs/lib/finite_sets/finite_sets_sum.pvs
-pvs/lib/finite_sets/finite_sets_sum_real.bin
 pvs/lib/finite_sets/finite_sets_sum_real.prf
+pvs/lib/finite_sets/finite_sets_sum_real.prf.bak
 pvs/lib/finite_sets/finite_sets_sum_real.pvs
-pvs/lib/finite_sets/func_composition.bin
 pvs/lib/finite_sets/func_composition.prf
 pvs/lib/finite_sets/func_composition.pvs
-pvs/lib/finite_sets/orphaned-proofs.prf
-pvs/lib/finite_sets/prelude_aux.bin
 pvs/lib/finite_sets/prelude_aux.prf
 pvs/lib/finite_sets/prelude_aux.pvs
-pvs/lib/finite_sets/top.bin
+pvs/lib/finite_sets/pvsbin/finite_cross.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_below.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_card_eq.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_eq.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_inductions.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_int.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_minmax.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_minmax_props.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_nat.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_pred.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_sum.bin
+pvs/lib/finite_sets/pvsbin/finite_sets_sum_real.bin
+pvs/lib/finite_sets/pvsbin/func_composition.bin
+pvs/lib/finite_sets/pvsbin/prelude_aux.bin
+pvs/lib/finite_sets/pvsbin/top.bin
 pvs/lib/finite_sets/top.prf
 pvs/lib/finite_sets/top.pvs
+pvs/lib/finite_sets/top_hier.ps
+pvs/lib/lift_adt.pvs
 pvs/lib/list_adt.pvs
 pvs/lib/ordstruct_adt.pvs
 pvs/lib/prelude.prf
 pvs/lib/prelude.pvs
 pvs/lib/pvs-language.help
 pvs/lib/pvs-prover.help
+pvs/lib/pvs-style.css
 pvs/lib/pvs.bnf
 pvs/lib/pvs.grammar
 pvs/lib/pvs.help
 pvs/lib/strategies.lisp
+pvs/lib/union_adt.pvs
 pvs/pvs
 pvs/pvs-tex.sub
 pvs/pvs.sty
@@ -632,12 +528,13 @@ pvs/wish/gray.xbm
 pvs/wish/pvs-support.tcl
 pvs/wish/sequent.xbm
 @dirrm pvs/wish
+@dirrm pvs/lib/finite_sets/pvsbin
 @dirrm pvs/lib/finite_sets
+@dirrm pvs/lib/bitvectors/pvsbin
 @dirrm pvs/lib/bitvectors
 @dirrm pvs/lib
 @dirrm pvs/emacs/xemacs21
 @dirrm pvs/emacs/emacs20
-@dirrm pvs/emacs/emacs19
 @dirrm pvs/emacs/emacs-src/ilisp
 @dirrm pvs/emacs/emacs-src
 @dirrm pvs/emacs
@@ -646,5 +543,6 @@ pvs/wish/sequent.xbm
 @dirrm pvs/bin/ix86-redhat5/runtime
 @dirrm pvs/bin/ix86-redhat5
 @dirrm pvs/bin
+@exec ${MKDIR} %D/pvs/Examples
 @dirrm pvs/Examples
 @dirrm pvs
diff --git a/devel/pvs/distinfo b/devel/pvs/distinfo
index 9ee1e0407dc..a1f85163a35 100644
--- a/devel/pvs/distinfo
+++ b/devel/pvs/distinfo
@@ -1,16 +1,13 @@
-$NetBSD: distinfo,v 1.5 2005/02/23 22:24:31 agc Exp $
+$NetBSD: distinfo,v 1.6 2005/09/02 02:27:11 jschauma Exp $
 
-SHA1 (pvs-3.1-linux.tgz) = 58a24515d06ab2a476efad593bd5b3768660797d
-RMD160 (pvs-3.1-linux.tgz) = 7c180330b39c3713ea70faa235973f4b19363c85
-Size (pvs-3.1-linux.tgz) = 13398586 bytes
-SHA1 (pvs-3.1-system.tgz) = 817736af58902c10e872e86981e767de93ae204d
-RMD160 (pvs-3.1-system.tgz) = 8a4e7743adec5cc43b56226a226a8b00192b0616
-Size (pvs-3.1-system.tgz) = 1306332 bytes
-SHA1 (pvs-3.1-emacs19.tgz) = fe936a5edbc3b3c5ce4d5131ca992ee275168d56
-RMD160 (pvs-3.1-emacs19.tgz) = 8aa83a0e1caeb62648fee2c78a2e25c601d0ec05
-Size (pvs-3.1-emacs19.tgz) = 360407 bytes
-SHA1 (pvs-3.1-libraries.tgz) = c8e9b79347d335eb7c8bd9dc489cef2073472509
-RMD160 (pvs-3.1-libraries.tgz) = a28c09b5bd2b138f5064f672136e1eeffa94aae9
-Size (pvs-3.1-libraries.tgz) = 1457926 bytes
-SHA1 (patch-aa) = 7199e499e1cd85da0c726b26416934fc222b3b46
-SHA1 (patch-ab) = b0f918f5fe054da223ea4c2698e1b9f58c5a684f
+SHA1 (pvs-3.2-linux.tgz) = 10b2db78aebfe0a66da514ebdc0180f57c686979
+RMD160 (pvs-3.2-linux.tgz) = d340cd68341ff845e00a1d940a4d315615eaf99a
+Size (pvs-3.2-linux.tgz) = 12350949 bytes
+SHA1 (pvs-3.2-system.tgz) = be9a57267ddc3ad241b1e26c55f2a60cff16d787
+RMD160 (pvs-3.2-system.tgz) = e69c8e0448e5973832912cf7f9a7cdf35612d705
+Size (pvs-3.2-system.tgz) = 1463623 bytes
+SHA1 (pvs-3.2-libraries.tgz) = 72fce592786a9d686e44aecd3c5355118aa15e02
+RMD160 (pvs-3.2-libraries.tgz) = 2087d70ebce0b4538f046ae0125b5c9db58f4d77
+Size (pvs-3.2-libraries.tgz) = 3719266 bytes
+SHA1 (patch-aa) = 10c4eaffbf6f0b571b2077958187e2abfae487f6
+SHA1 (patch-ab) = 2e626ed30fca3dffb708634b7b2a98c7359184ed
diff --git a/devel/pvs/files/MESSAGE b/devel/pvs/files/MESSAGE
index cbbf4e4a5eb..1c8ae05365f 100644
--- a/devel/pvs/files/MESSAGE
+++ b/devel/pvs/files/MESSAGE
@@ -1,7 +1,7 @@
-==============================================================================
-$NetBSD: MESSAGE,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+===========================================================================
+$NetBSD: MESSAGE,v 1.2 2005/09/02 02:27:11 jschauma Exp $
 
 	The PVS Specification and Verification System requires a kernel
 	built with 'COMPAT_LINUX' and 'PROCFS' enabled.
 
-==============================================================================
+===========================================================================
diff --git a/devel/pvs/patches/patch-aa b/devel/pvs/patches/patch-aa
index 3c2434ffcb5..6af189dd704 100644
--- a/devel/pvs/patches/patch-aa
+++ b/devel/pvs/patches/patch-aa
@@ -1,29 +1,26 @@
-$NetBSD: patch-aa,v 1.3 2003/03/31 20:49:36 jschauma Exp $
+$NetBSD: patch-aa,v 1.4 2005/09/02 02:27:12 jschauma Exp $
 
---- pvs.orig	Thu Dec 19 22:38:25 2002
-+++ pvs	Thu Dec 19 22:42:32 2002
-@@ -46,7 +46,7 @@
+--- pvs.orig	2004-10-05 20:04:54.000000000 -0400
++++ pvs	2005-09-01 10:51:21.000000000 -0400
+@@ -45,7 +45,7 @@
  
  # PVSPATH should be set after installation by <PVS>/bin/relocate or by hand
  # to the location of the PVS installation
--PVSPATH=/project/pvs/pvs3.0
+-PVSPATH=/homes/owre/pvs3.0
 +PVSPATH=@PREFIX@/pvs
  
  #-------------------------------------------------
  # Nothing below this line should need modification
-@@ -167,6 +167,11 @@
+@@ -162,7 +162,7 @@
  	    then echo "PVS 3.0 only runs under Solaris or Linux"; exit 1
  	 fi
  	 PVSARCH=sun4;;
-+  NetBSD) # pretend to be a redhat linux system
-+	opsys=redhat
-+	majvers=5
-+	othervers=4
-+	PVSARCH=ix86;;
-   Linux) # If Linux, we need to determine the Redhat version to use.
+-  Linux) # If Linux, we need to determine the Redhat version to use.
++  Linux|NetBSD) # If Linux, we need to determine the Redhat version to use.
  	 opsys=redhat
- 	 if [ ! $majvers ]; then
-@@ -228,8 +233,15 @@
+ 	 majvers=5
+ 	 othervers=4 
+@@ -215,8 +215,15 @@
  PVSIMAGE="$PVSLISP"
  
  export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH
diff --git a/devel/pvs/patches/patch-ab b/devel/pvs/patches/patch-ab
index c10d48ba9f2..4ffbef64c59 100644
--- a/devel/pvs/patches/patch-ab
+++ b/devel/pvs/patches/patch-ab
@@ -1,18 +1,18 @@
-$NetBSD: patch-ab,v 1.1 2003/06/25 21:01:36 seb Exp $
+$NetBSD: patch-ab,v 1.2 2005/09/02 02:27:12 jschauma Exp $
 
---- doc/release-notes/pvs-release-notes.info.orig	Sat Feb 15 05:37:27 2003
-+++ doc/release-notes/pvs-release-notes.info
+--- doc/release-notes/pvs-release-notes.info.orig	2004-11-04 03:54:45.000000000 -0500
++++ doc/release-notes/pvs-release-notes.info	2005-09-01 10:53:02.000000000 -0400
 @@ -1,6 +1,13 @@
- This is pvs-release-notes.info, produced by makeinfo version 4.0 from
+ This is pvs-release-notes.info, produced by makeinfo version 4.7 from
  pvs-release-notes.texi.
  
 +INFO-DIR-SECTION Programming & development tools
 +START-INFO-DIR-ENTRY
-+* PVS Release notes: (pvs-release-notes).      PVS Specification and
-+                                               Verification System release
-+                                               notes.
++* PVS Release notes: (pvs-release-notes).	PVS Specification and
++						Verification System release
++						notes.
 +END-INFO-DIR-ENTRY
 +
- This file contains the release notes for PVS version 3.0
+ This file contains the release notes for PVS versions 3.0 - 3.2
  
  Copyright 2002 SRI International