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

library path




The manual explains how to declare a path for a library 
and import something startring with this path:
fs: LIBRARY = "xxx/PVS/lib/finite_sets"
IMPORTING fs@finite_sets

My problem arises when I want to import a theory in the
heading of a theory:

e_r[Ix,D:TYPE, (IMPORTING finite_sets[Ix]) c:finite_set[Ix]]: THEORY
BEGIN
...
END e_r

works if finite_sets is already known. 

But does not work otherwhise. It does not seem possible
to specificy a library path in the heading of a theory?

thanks.