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

[PVS] IMPORTINGs in theory parameter list



Hello all,

Is it possible to import theories from a library
the formal parameter list of a theory? When the
importing clause in inside a theory, there is no
problem:

   th : THEORY
   BEGIN
     lib : LIBRARY = "~/pvslib"
    IMPORTING lib@mylib
   ...
   END th

I would like to do the same thing but with the
importing clause in the parameter list I don't see
any place to put the declaration of lib:

   th : THEORY[(IMPORTING mylib)]
   BEGIN
    ...
   END th
-- 
Pertti