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

Re: User libraries in the PVS lib directory


> 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".


	- 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