library importings

[Marieke Huisman <Marieke.Huisman@sophia.inria.fr>]

Hi,

I have two questions about library importings.

I have generated two PVS specifications, one of a defensive virtual 
machine, one of an offensive one. These specifications have many 
datatype and theory names in common, so to avoid conflicts I've put 
them in two directories:
Offensive and Defensive.

I try to import these as two different libraries:

  defensive : LIBRARY = "Defensive"
  offensive : LIBRARY = "Offensive"

  IMPORTING defensive@nEG_def,
            offensive@nEG_def

When I try this with a small example, but here I get two problems:

- I have constructed .bin files in the Defensive and Offensive 
directories, but sometimes PVS does not only restore the bin files, 
but also starts to typecheck, and then it returns with a typecheck 
problem.

- In case PVS does not produce a type check problem, it restores all 
the bin files and finally produces the following error:

Error: the assertion ITHEORY failed.

Are there ways I can avoid these problems? Are there better ways to 
do these importings?
Any help would be appreciated!

Thanks,

Marieke Huisman