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

Re: User libraries in the PVS lib directory




Theories in the lib subdirectory are not extensions to the prelude,
they are just a convenient repository and don't require a LIBRARY
clause.

Look at the documentation for M-x load-prelude-library to see how to
extend the prelude with a specified context.

Note that it is not necessary to specifically give IMPORTING clauses for
things in the prelude - they are imported into the current context anyway.

Dave

---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com