[opentheory-users] assumption refuses to be satisfied

[Ramana Kumar]

I am having trouble constructing an OpenTheory package. Perhaps I have
misunderstood the package specification language.

This is my situation. (I have omitted some details for the moment, but I
can provide the actual article files etc. if necessary.)

I have two articles, art1.art and art2.art.

I can run opentheory info on each of them to see what they assume and what
they prove.

opentheory info art1.art:
2 external type operators: ...
9 external constants: ...
6 assumptions: ... [all of these are in base]
2 theorems: th1, th2

opentheory info art2.art:
2 external type operators: ...
17 external constants: ...
27 assumptions: th1, th2, [all the rest are in base]
4 defined constants: ...
41 theorems: ...

(th1 and th2 do not mention any of the defined constants.)

Now, I make the following package, pkg.thy.
requires: base
a {
article: "art1.art"
}
main {
import: a
article: "art2.art"
}

opentheory info pkg.thy:
2 external type operators: ...
17 external constants: ...
26 satisfied assumptions: hidden
1 unsatisfied assumption: th1
4 defined constants: ...
41 theorems: ...

Why is th1 still unsatisfied? I expected no unsatisfied assumptions.

What could be going wrong?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151102/e9b06562/attachment.html>