[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

   th : THEORY
     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)]
   END th