[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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"
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
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?