[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: User libraries in the PVS lib directory


Thanks for your reply. We are familiar with this approach. My question was
specific to the PVS 'lib' directory. Can we put theories in this directory
and access them as "IMPORTING UserTheory", as we would a theory in the
prelude? We could not find any information on whether this is possible or

We appreciate your help. Thanks. Bye.

On Mon, 26 Jul 1999, Holger PFEIFER wrote:

> Murali,
> > We are trying to place some theories written by us in the 'lib' directory
> > of our PVS installation. We assumed that we should be able to import these
> > theories by writing "importing UserTheory". But this does not seem to work
> > - PVS is unable to find this theory. 
> You need to put your theories into a subdirectory, say 'local', of the 'lib' directory.
> Make sure that this subdirectory contains a context file (.pvscontext), either by copying
> it or by re-typechecking your new library theories. After a restart of PVS you should be
> able to access the theories 
> by writing "IMPORTING local@UserTheory".
> Regards,
> 	- Holger
> -- 
> ----------------------------------------------------------------------
> Holger Pfeifer                              Tel.: (+49) 731 / 502-4124
> Universitaet Ulm                             Fax: (+49) 731 / 502-4119
> Abt. Kuenstliche Intelligenz          pfeifer@ki.informatik.uni-ulm.de
> D-89069 Ulm           http://www.informatik.uni-ulm.de/ki/pfeifer.html   
> ----------------------------------------------------------------------

Best Wishes,
	-- Murali
Murali Rangarajan  #  rmurali@ececs.uc.edu # http://www.ececs.uc.edu/~rmurali
Knowledge Based Software Engineering Lab   #   finger machines : ella, evans
Phone:           R-(513) 872 0878          #          O-(513) 556 0267 

"The most difficult thing in the world is to know how to do a thing and
to watch someone else do it wrong without comment."
                -- Theodore H. White

The safest way to double your money is to fold it over and put it in your 
pocket. -Kin Hubbard