<div dir="ltr"><div>I am having trouble constructing an OpenTheory package. Perhaps I have misunderstood the package specification language.<br><br></div><div>This is my situation. (I have omitted some details for the moment, but I can provide the actual article files etc. if necessary.)<br><br></div><div>I have two articles, art1.art and art2.art.<br><br></div><div>I can run opentheory info on each of them to see what they assume and what they prove.<br><br></div><div>opentheory info art1.art:<br></div><div>2 external type operators: ...<br></div><div>9 external constants: ...<br></div><div>6 assumptions: ... [all of these are in base]<br></div><div>2 theorems: th1, th2<br></div><div><br></div><div>opentheory info art2.art:<br></div><div>2 external type operators: ...<br></div><div>17 external constants: ...<br></div><div>27 assumptions: th1, th2, [all the rest are in base]<br></div><div>4 defined constants: ...<br></div><div>41 theorems: ...<br><br></div><div>(th1 and th2 do not mention any of the defined constants.)<br><br></div><div>Now, I make the following package, pkg.thy.<br></div><div>requires: base<br>a {<br></div><div>article: "art1.art"<br>}<br></div><div>main {<br></div><div>import: a<br></div><div>article: "art2.art"<br>}<br><br></div><div>opentheory info pkg.thy:<br></div><div>2 external type operators: ...<br></div><div>17 external constants: ...<br></div><div>26 satisfied assumptions: hidden<br></div><div>1 unsatisfied assumption: th1<br></div><div>4 defined constants: ...<br></div><div>41 theorems: ...<br><br></div><div>Why is th1 still unsatisfied? I expected no unsatisfied assumptions.<br></div><div><br></div><div>What could be going wrong?<br></div></div>