[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
The mucalculus is part of the prelude as of PVS version 2.3, but the
library dump files have not all been converted yet.
Just comment out the importing of MU@ctlops and it should work.
> From: Jean-François Molderez <firstname.lastname@example.org>
> Subject: MU.pvs
> Date: Wed, 18 Sep 2002 16:31:07 +0200
> To: <email@example.com>
> [1 <text/plain; iso-8859-1 (quoted-printable)>]
> I don't find the file MU.pvs in my directory pvs/lib/ (when trying to reproduce example in
> chap 4 p54 State Transition Systems and SCR Requirements Specifications)
> JF Molderez (firstname.lastname@example.org)
> [2 <text/html; iso-8859-1 (quoted-printable)>]
- From: Jean-François Molderez <email@example.com>